diff --git a/.config/dotnet-tools.json b/.config/dotnet-tools.json index e66fab2a4..9a2479351 100644 --- a/.config/dotnet-tools.json +++ b/.config/dotnet-tools.json @@ -15,16 +15,10 @@ ] }, "dotnet-ilverify": { - "version": "8.0.0", + "version": "10.0.11", "commands": [ "ilverify" ] - }, - "microsoft.coyote.cli": { - "version": "1.7.11", - "commands": [ - "coyote" - ] } } } \ No newline at end of file diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml index 3c5c097b8..5d64d2b56 100644 --- a/.github/workflows/codeql-analysis.yml +++ b/.github/workflows/codeql-analysis.yml @@ -26,6 +26,10 @@ jobs: uses: NuGet/setup-nuget@v1 with: nuget-version: '6.x' + - name: Setup .NET 10.0 SDK + uses: actions/setup-dotnet@v1 + with: + dotnet-version: '10.0.x' - name: Setup .NET 8.0 SDK uses: actions/setup-dotnet@v1 with: diff --git a/.github/workflows/test-coyote.yml b/.github/workflows/test-coyote.yml index ce2812d21..b7d2e59dd 100644 --- a/.github/workflows/test-coyote.yml +++ b/.github/workflows/test-coyote.yml @@ -30,6 +30,10 @@ jobs: uses: NuGet/setup-nuget@v1 with: nuget-version: '6.x' + - name: Setup .NET 10.0 SDK + uses: actions/setup-dotnet@v1 + with: + dotnet-version: '10.0.303' - name: Setup .NET 8.0 SDK uses: actions/setup-dotnet@v1 with: @@ -48,9 +52,14 @@ jobs: - name: Build Coyote projects run: ./Scripts/build.ps1 -ci -nuget shell: pwsh + - name: Run native host compatibility matrix + run: ./Tests/Compatibility/run-compatibility-matrix.ps1 + shell: pwsh - name: Validate Coyote rewriting if: ${{ matrix.platform == 'windows-latest' }} - run: ./Tests/compare-rewriting-diff-logs.ps1 + run: | + ./Tests/compare-rewriting-diff-logs.ps1 -framework net10.0 + ./Tests/compare-rewriting-diff-logs.ps1 -framework net8.0 shell: pwsh - name: Run Coyote tests run: ./Scripts/run-tests.ps1 -ci @@ -83,6 +92,10 @@ jobs: COYOTE_CLI_TELEMETRY_OPTOUT: 1 steps: - uses: actions/checkout@v2 + - name: Setup .NET 10.0 SDK + uses: actions/setup-dotnet@v1 + with: + dotnet-version: '10.0.303' - name: Setup .NET 8.0 SDK uses: actions/setup-dotnet@v1 with: diff --git a/.github/workflows/test-performance.yml b/.github/workflows/test-performance.yml index 3482ef588..95e6e597b 100644 --- a/.github/workflows/test-performance.yml +++ b/.github/workflows/test-performance.yml @@ -23,6 +23,10 @@ jobs: uses: NuGet/setup-nuget@v1 with: nuget-version: '6.x' + - name: Setup .NET 10.0 SDK + uses: actions/setup-dotnet@v1 + with: + dotnet-version: '10.0.x' - name: Setup .NET 8.0 SDK uses: actions/setup-dotnet@v1 with: diff --git a/Common/build.props b/Common/build.props index 5cdeb0db7..e4e9986aa 100644 --- a/Common/build.props +++ b/Common/build.props @@ -16,10 +16,13 @@ LICENSE $(MSBuildThisFileDirectory)/../bin/nuget + + 14.0 + 10.0 - + 8.0 @@ -44,7 +47,7 @@ false true true - net8.0 + net10.0;net8.0 $(TargetFrameworks);netstandard2.0 $(TargetFrameworks);net6.0 diff --git a/NET10-COMPATIBILITY-ASSESSMENT.md b/NET10-COMPATIBILITY-ASSESSMENT.md new file mode 100644 index 000000000..de2f79c04 --- /dev/null +++ b/NET10-COMPATIBILITY-ASSESSMENT.md @@ -0,0 +1,324 @@ +# Coyote compatibility assessment for .NET 10 assemblies + +**Assessment date:** 2026-08-20 +**Repository:** `microsoft/coyote` +**Branch / commit:** `main` / `f2c135d201341ee5eff3d82cac62bdb85b25139f` +**Coyote version:** 1.7.11 (`Common/version.props:5`) +**Probe SDK/runtime:** .NET SDK 10.0.303, .NET runtime 10.0.11, C# 14 + +**Implementation plan:** [NET10-UPGRADE-PLAN.md](NET10-UPGRADE-PLAN.md) + +## Outcome + +Current Coyote can **parse and rewrite many `net10.0` assemblies**, and its existing `net8.0` binaries can execute under the .NET 10 runtime. It cannot, however, be considered generally compatible with arbitrary .NET 10 / C# 14 concurrency code today. + +The normal `coyote test` host is a `net8.0` process and fails to load a `net10.0` test assembly. A manual `dotnet exec` host override makes a baseline probe work. Once hosted on .NET 10, the rewriter still has concrete semantic coverage gaps for newer APIs and compiler lowering, including `Task.WhenAll(ReadOnlySpan)` and `System.Threading.Lock`. The latter is especially risky because it remains unreplaced without being reported as uncontrolled. + +**Decision:** use against `net10.0` only as a constrained workaround, not as declared/sound .NET 10 support. Proper support requires a native .NET 10 host plus rewriter/API coverage work and regression tests. + +## Direct answer + +| Question | Answer | +|---|---| +| Can a `net10.0` project reference current Coyote assemblies? | **Yes.** The probe compiled against the existing `net8.0` Coyote binaries. `net10.0` is compatible with lower `netX.0` assets. | +| Can current Coyote rewrite a `net10.0` assembly? | **Yes for the tested assembly.** Mono.Cecil 0.11.4 parsed and rewrote C# 14 async state machines and emitted a valid modified assembly. This does not prove every new metadata shape is supported. | +| Does normal `coyote test MyNet10.dll` work? | **No.** The `net8.0` host cannot load `System.Runtime, Version=10.0.0.0`. | +| Is there a usable-today workaround? | **Yes, constrained.** Run the existing CLI under the installed .NET 10 runtime with `dotnet exec --fx-version 10.0.11 --roll-forward LatestMajor ...`. | +| Is arbitrary .NET 10/C# 14 concurrency code controlled correctly? | **No.** New overloads and lowering can bypass Coyote's exact-signature wrappers. Two concrete gaps were reproduced. | +| Is C# 14 itself broadly incompatible? | **No evidence of a general language-version incompatibility.** The risk is feature-specific emitted IL and calls to new runtime APIs. | + +## Scope and method + +The assessment used four evidence sources: + +1. Static inspection of target frameworks, CLI runtime configuration, dependency conditions, rewriting type maps, method matching, wrappers, scripts, tests, and CI. +2. A baseline `net10.0` / C# 14 probe using `Task.Run`, `Task.Yield`, async state machines, `Monitor`-lowered `lock`, and an explicitly selected array overload of `Task.WhenAll`. +3. A new-API probe using `System.Threading.Lock` and the C# 14-selected `Task.WhenAll(ReadOnlySpan)` overload. +4. A forced `net10.0` build of the Coyote solution to identify native-retargeting failures. + +This is a compatibility assessment, not an implementation. No Coyote source code was changed. + +## Finding 1 — The published/test host is .NET 8, so normal execution fails + +**Severity:** blocking for normal CLI use +**Confidence:** high; reproduced + +The shared build targets declare `net8.0` as the primary target (`Common/build.props:47`). The tool project imports those targets (`Tools/Coyote/Coyote.csproj:18`). Its generated runtime configuration requests `Microsoft.NETCore.App` and `Microsoft.AspNetCore.App` 8.0 (`bin/net8.0/coyote.runtimeconfig.json:3-12`). + +Running the existing CLI normally against the rewritten `net10.0` probe failed during test discovery: + +```text +Microsoft (R) Coyote version 1.7.11.0 for .NET 8.0.30 +Unable to load one or more of the requested types. +Could not load file or assembly 'System.Runtime, Version=10.0.0.0 ...' +``` + +That is expected runtime-host behavior: an application hosted on .NET 8 cannot load assemblies compiled against .NET 10 reference assemblies. + +A manual host override succeeded: + +```powershell +dotnet exec --fx-version 10.0.11 --roll-forward LatestMajor ` + \bin\net8.0\coyote.dll ` + test .\bin\Debug\net10.0\Net10CoyoteProbe.dll -i 10 +``` + +Observed result: + +```text +Microsoft (R) Coyote version 1.7.11.0 for .NET 10.0.11 +Found 0 bugs. +Explored 10 execution paths: 10 fair, 0 unfair, 10 unique. +Controlled 50 operations: 5 (min), 5 (avg), 5 (max). +``` + +This proves the existing assemblies can run under .NET 10. It is a workaround, not a normal supported tool invocation or package contract. + +## Finding 2 — Basic C# 14 async IL is rewriteable + +**Severity:** positive compatibility evidence +**Confidence:** high for the tested patterns + +The baseline probe was built by SDK 10.0.303 with `TargetFramework=net10.0` and `LangVersion=14.0`. Coyote's .NET 8 rewriter successfully: + +- read the assembly; +- rewrote `AsyncTaskMethodBuilder` to Coyote's builder; +- rewrote task awaiters and `Task.Run`; +- rewrote `Task.Yield`; +- rewrote ordinary object-based `lock` through the existing `Monitor` wrapper; +- wrote the modified `net10.0` assembly and an IL diff. + +The compiler-generated async state-machine shape was therefore not intrinsically incompatible. Coyote's type map explicitly covers async builders and awaiters (`Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs:30-62`) and task/thread synchronization types (`TypeRewritingPass.cs:64-90`). + +This finding should not be generalized to every C# 13/14 feature. Coyote rewrites exact emitted types and method signatures; language features that change lowering or overload selection can evade those mappings. + +## Finding 3 — C# 14 selects a `Task.WhenAll` overload Coyote does not wrap + +**Severity:** high; produces uncontrolled work and weakens systematic exploration +**Confidence:** high; reproduced + +In the new-API probe, this source: + +```csharp +await Task.WhenAll(first, second); +``` + +compiled to: + +```text +Task.WhenAll(ReadOnlySpan) +``` + +The emitted IL used a compiler-generated inline array, converted it to `ReadOnlySpan`, and called the span overload. Microsoft documents that C# 14 makes span-based overloads applicable in more scenarios. The span overload itself is available in .NET 9 and later. + +Coyote's wrapper contains only array and `IEnumerable` forms for `WhenAll` (`Source/Test/Rewriting/Types/Threading/Tasks/Task.cs:219-256`). There is no `ReadOnlySpan` or generic `ReadOnlySpan>` wrapper. + +The rewritten IL retained the runtime call and injected `ThrowIfReturnedTaskNotControlled` rather than replacing it with a controlled Coyote call. Execution completed but reported: + +```json +{"UncontrolledInvocations":["System.Threading.Tasks.Task.WhenAll"]} +``` + +Explicitly selecting the old overload avoids the gap: + +```csharp +await Task.WhenAll(new Task[] { first, second }); +``` + +That workaround ran with zero uncontrolled invocations. + +Related static gaps in the .NET 10 `Task` surface include: + +- `WhenAll(ReadOnlySpan)` and the generic equivalent; +- `WhenAny(ReadOnlySpan)` and the generic equivalent; +- `WaitAll(ReadOnlySpan)`; +- all `Task.WhenEach(...)` overloads introduced in .NET 9; +- `Task.Delay(..., TimeProvider, ...)`; +- instance `Task.WaitAsync(...)` overloads. + +Not every missing wrapper is new to .NET 10, but these APIs are part of the current `net10.0` surface and should be audited for intended Coyote semantics. + +## Finding 4 — `System.Threading.Lock` is silently outside Coyote control + +**Severity:** critical soundness risk for code using the recommended modern lock type +**Confidence:** high that it is not rewritten; runtime consequences require dedicated stress tests + +Starting with .NET 9 and C# 13, Microsoft recommends `System.Threading.Lock`. When the compiler knows the operand has that type, a `lock` statement lowers to approximately: + +```csharp +using (syncObject.EnterScope()) +{ + // critical section +} +``` + +It does **not** lower to `Monitor.Enter` / `Monitor.Exit`. + +Coyote's rewrite map covers `Monitor`, `SemaphoreSlim`, `Interlocked`, wait handles, and related older primitives, but has no `System.Threading.Lock` entry (`Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs:78-90`). A repository search found no `System.Threading.Lock` or `EnterScope` implementation. + +The rewritten probe IL still contained: + +```text +System.Threading.Lock::EnterScope() +System.Threading.Lock/Scope::Dispose() +``` + +Coyote's uncontrolled-invocation pass does not classify `System.Threading.Lock` as uncontrolled. Its threading checks cover selected `Thread`, `ThreadPool`, and event-handle methods (`Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs:115-149`), but not `Lock`. + +Therefore, code can appear to run under Coyote without a warning while lock acquisition and release remain outside the scheduler's model. Coyote may still inject scheduling points around memory accesses, but that is not equivalent to controlling the synchronization primitive and can permit real blocking or miss relevant schedules. + +Using a dedicated `object` lock forces the older `Monitor` lowering and stays on the currently modeled path. + +## Finding 5 — Rewriter coverage is exact-signature driven + +**Severity:** architectural source of future compatibility gaps +**Confidence:** high; code inspection + +The type rewriter maps known BCL type names to Coyote replacement types (`TypeRewritingPass.cs:18-20`, `30-111`). Method replacement then requires a matching method name, static/instance form, parameter count, and parameter full names (`MethodBodyTypeRewritingPass.cs:168-223`, `380-426`). + +That architecture works well for known signatures but does not automatically inherit support when .NET adds overloads or the compiler starts choosing a different overload. The `ReadOnlySpan` result is a direct example. + +Compatibility testing should therefore be source-pattern based as well as API-list based: compile representative concurrency syntax with each supported SDK/language version, inspect the emitted calls, rewrite it, and assert there are no uncontrolled invocations. + +## Finding 6 — Native `net10.0` retargeting is incomplete + +**Severity:** blocking for shipping a native .NET 10 tool asset +**Confidence:** high; reproduced and statically confirmed + +A forced solution build with SDK 10.0.303 and `TargetFrameworks=net10.0` restored successfully after switching to the requested package source. Results: + +- `Source/Core` compiled to `bin/net10.0/Microsoft.Coyote.dll`; +- `Source/Actors` compiled to `bin/net10.0/Microsoft.Coyote.Actors.dll`; +- `Source/Test` failed because `Microsoft.Extensions.DependencyModel` was absent. + +`Source/Test/Test.csproj` only adds that dependency for `net8.0` and `net6.0` (`Test.csproj:22-27`). The CLI/tool projects likewise only add framework references for those exact TFMs (`Tools/Coyote/Coyote.csproj:25-38`, `Tools/CLI/Coyote.CLI.csproj:23-30`). + +Additional retargeting work identified by static inspection: + +- `global.json` pins SDK 8.0.404 (`global.json:3`); +- `Common/build.props` gives `net10.0` the fallback C# 8 language version because only `net8.0` and `net6.0` receive C# 10 (`Common/build.props:19-23`); +- `Scripts/run-tests.ps1` rejects `net10.0` and hard-codes `net8.0` ILVerify paths (`Scripts/run-tests.ps1:5-6`, `62-69`); +- CI installs/tests .NET 8 and legacy .NET 6, not .NET 10 (`.github/workflows/test-coyote.yml:33-40`, `80-83`; `.github/workflows/codeql-analysis.yml:29-32`; `.github/workflows/test-performance.yml:26-29`); +- the .NET 10 restore reports `NU1510` for the unconditional `System.Threading.Tasks.Extensions` reference in `Source/Core/Core.csproj:17`. + +## Finding 7 — Existing tests cannot detect the demonstrated C# 14 gap + +**Severity:** high regression risk +**Confidence:** high; code inspection + +`Tests/Tests.Rewriting/Types/TaskRewritingTests.cs:17-27` calls `Task.WhenAll(Task.CompletedTask)` and the generic equivalent. Under the repository's `net8.0` / C# 10 build, these compile to the existing array overload and pass through the current wrapper. + +There is no test compiled under C# 14 that verifies the overload actually selected by the newer compiler. There is also no test for `System.Threading.Lock` lowering. The current tests validate known wrapper behavior, not cross-SDK source compatibility. + +## Compatibility classification + +### Works today with the forced .NET 10 host + +- Loading current Coyote `net8.0` libraries from a `net10.0` process. +- Reading and writing the tested .NET 10 assembly with Mono.Cecil 0.11.4. +- Standard async `Task` state machines. +- `Task.Run`, `Task.Yield`, awaiters, and existing wrapped signatures. +- Object-based `lock` lowered through `Monitor`. + +### Workaround-only + +- Running `coyote test` against a `net10.0` assembly by forcing the existing CLI onto .NET 10. +- Avoiding span overloads by explicitly constructing arrays or casting to an older signature. +- Avoiding `System.Threading.Lock` and using an object-backed `Monitor` lock. + +### Not controlled or not supported + +- Normal .NET 8-hosted CLI loading a .NET 10 assembly. +- `Task.WhenAll(ReadOnlySpan)` in the reproduced C# 14 case. +- `System.Threading.Lock` acquisition/release. +- Other unwrapped .NET 9/10 Task overloads until individually implemented and tested. + +## Required upgrades + +### P0 — minimum credible .NET 10 support + +1. **Ship a native `net10.0` CLI/tool asset.** Update the SDK pin, shared target matrix, framework references, dependency conditions, scripts, and package layout. Do not rely on users knowing the `dotnet exec` host override. +2. **Add wrappers for span-based Task combinators.** At minimum cover generic/non-generic `WhenAll` and `WhenAny`, plus span-based `WaitAll` where Coyote intends to control blocking waits. +3. **Model `System.Threading.Lock`.** Add rewrite mapping/interception for `EnterScope`/scope disposal, or explicitly reject it as uncontrolled until sound modeling exists. Silent pass-through is the worst current behavior. +4. **Add .NET 10/C# 14 compiled probes to CI.** Assert successful discovery/execution and zero uncontrolled invocations for supported source patterns. + +### P1 — complete current Task surface audit + +1. Decide and test semantics for `Task.WhenEach`. +2. Decide and test `Task.WaitAsync` and `TimeProvider`-based delay APIs. +3. Generate an API-diff checklist between supported runtime versions and Coyote wrapper types so newly added overloads cannot silently escape coverage. +4. Test both direct API calls and compiler-selected overloads from ordinary source syntax. + +### P2 — hardening + +1. Add a startup diagnostic when the CLI host runtime is older than the target assembly runtime, replacing the current reflection loader failure with an actionable message. +2. Consider treating unknown synchronization types/methods as explicit uncontrolled invocations rather than silently allowing them. +3. Validate Mono.Cecil against a wider corpus of .NET 10 assemblies and new metadata shapes before deciding whether its version must be upgraded. The basic probe does not itself require an upgrade. +4. Remove or condition packages that trigger .NET 10 package-pruning warnings. + +## Recommended policy for users today + +If immediate use is unavoidable: + +1. Install the matching .NET 10 runtime. +2. Run Coyote via the explicit .NET 10 host override. +3. Avoid `System.Threading.Lock`. +4. Avoid implicit binding to span-based Task overloads; select array or enumerable overloads explicitly. +5. Treat any uncontrolled invocation report as a failed compatibility check, not a warning to ignore. +6. Run a representative smoke suite before trusting exploration results. + +This policy is operationally possible but fragile. It should not be advertised as full .NET 10 support. + +## Plan + +1. Establish the current supported host/TFM/package contract from project and CI files. +2. Audit rewriter coverage against .NET 9/10 concurrency and C# 13/14 lowering changes. +3. Reproduce current behavior with a pinned `net10.0`/C# 14 probe. +4. Classify findings as supported, workaround-only, uncontrolled, or blocked. +5. Write and verify a persistent markdown assessment report; no product implementation changes. + +## Execution log + +- **Step 1 — host/TFM contract:** inspected shared targets, tool projects, runtime config, scripts, and CI; verified the shipped host is `net8.0` and no native .NET 10 path exists. +- **Step 2 — rewriter audit:** inspected the known type map, exact method matching, task wrappers, uncontrolled-invocation pass, and rewriting tests; identified concrete missing signatures and silent `Lock` handling. +- **Step 3 — probes:** built two assemblies with SDK 10.0.303/C# 14, rewrote both, tested default and forced hosts, and inspected original/rewritten IL. +- **Step 4 — classification:** separated verified baseline support, host workaround, reproduced semantic gaps, and static-audit candidates. +- **Step 5 — report:** recorded evidence and prioritized required upgrades here. + +## Files / ids touched + +- `NuGet.config` — previously replaced at the user's request; unrelated to Coyote compatibility logic. +- `coyote-net10-compatibility-assessment-20260820` — this report artifact. +- No Coyote product source files were modified by the assessment. + +## Verification + +- Repository's standard .NET 8 build succeeded after removing one SDK-10-generated stale `project.assets.json` file. +- Baseline .NET 10 probe build: succeeded under SDK 10.0.303. +- Baseline rewrite: succeeded and emitted modified assembly/IL diff. +- Default-host test: failed loading `System.Runtime, Version=10.0.0.0`. +- Forced-.NET-10-host baseline test: succeeded, 10 paths, 50 controlled operations, zero uncontrolled invocations. +- New-API probe build/rewrite: succeeded. +- Rewritten IL retained `System.Threading.Lock::EnterScope()` and `Task.WhenAll(ReadOnlySpan)`. +- New-API test: completed but reported one uncontrolled invocation, `System.Threading.Tasks.Task.WhenAll`. +- Forced native `net10.0` Coyote build: Core and Actors succeeded; Test failed on missing `Microsoft.Extensions.DependencyModel` references. + +## Sources + +- Microsoft, [Select which .NET version to use](https://learn.microsoft.com/dotnet/core/versions/selection) +- Microsoft, [Target frameworks in SDK-style projects](https://learn.microsoft.com/dotnet/standard/frameworks) +- Microsoft, [C# 14 overload resolution with span parameters](https://learn.microsoft.com/dotnet/core/compatibility/core-libraries/10.0/csharp-overload-resolution) +- Microsoft, [The `lock` statement](https://learn.microsoft.com/dotnet/csharp/language-reference/statements/lock) +- Microsoft, [`Task.WhenAll` overloads for .NET 10](https://learn.microsoft.com/dotnet/api/system.threading.tasks.task.whenall?view=net-10.0) +- Microsoft, [`Task.WhenEach` for .NET 10](https://learn.microsoft.com/dotnet/api/system.threading.tasks.task.wheneach?view=net-10.0) + +## Deferred / open + +- Full implementation is intentionally out of scope. +- This assessment did not exhaustively execute every Coyote wrapper against every .NET 10 overload. +- `System.Threading.Lock` needs a focused design because its `ref struct` scope and blocking semantics differ from a simple static method wrapper. +- Broader Mono.Cecil validation should include assemblies using newer metadata features beyond the tested async/inline-array patterns. + +## Suggested next + +Turn the P0 section into an implementation plan with four independently verifiable workstreams: native host/packaging, Task span overloads, `System.Threading.Lock`, and cross-SDK CI probes. diff --git a/Samples/.config/dotnet-tools.json b/Samples/.config/dotnet-tools.json new file mode 100644 index 000000000..ea5e81975 --- /dev/null +++ b/Samples/.config/dotnet-tools.json @@ -0,0 +1,12 @@ +{ + "version": 1, + "isRoot": true, + "tools": { + "microsoft.coyote.cli": { + "version": "1.7.11", + "commands": [ + "coyote" + ] + } + } +} diff --git a/Samples/Scripts/build-tests.ps1 b/Samples/Scripts/build-tests.ps1 index e1bf3832d..a3c5abb3a 100644 --- a/Samples/Scripts/build-tests.ps1 +++ b/Samples/Scripts/build-tests.ps1 @@ -13,7 +13,7 @@ Write-Comment -prefix "." -text "Building the Coyote samples" -color "yellow" if ($local.IsPresent -and $nuget.IsPresent) { # Restore the local coyote tool. - &dotnet tool restore + &dotnet tool restore --tool-manifest "$PSScriptRoot/../.config/dotnet-tools.json" } # Check that the expected .NET SDK is installed. diff --git a/Samples/Scripts/build.ps1 b/Samples/Scripts/build.ps1 index 4f7f15b8a..b479770ed 100644 --- a/Samples/Scripts/build.ps1 +++ b/Samples/Scripts/build.ps1 @@ -13,7 +13,7 @@ Write-Comment -prefix "." -text "Building the Coyote samples" -color "yellow" if ($local.IsPresent -and $nuget.IsPresent) { # Restore the local coyote tool. - &dotnet tool restore + &dotnet tool restore --tool-manifest "$PSScriptRoot/../.config/dotnet-tools.json" } # Check that the expected .NET SDK is installed. diff --git a/Scripts/CI/azure-nuget-sign-publish.yml b/Scripts/CI/azure-nuget-sign-publish.yml index 03c9347fa..c624bd9b5 100644 --- a/Scripts/CI/azure-nuget-sign-publish.yml +++ b/Scripts/CI/azure-nuget-sign-publish.yml @@ -7,6 +7,11 @@ steps: inputs: versionSpec: 6.x +- task: UseDotNet@2 + displayName: 'Install .NET 10.0 SDK' + inputs: + version: 10.0.x + - task: UseDotNet@2 displayName: 'Install .NET 8.0 SDK' inputs: @@ -33,6 +38,36 @@ steps: failOnStderr: true pwsh: true +- task: EsrpCodeSigning@2 + displayName: 'ESRP CodeSigning .NET 10.0' + inputs: + ConnectedServiceName: CoyoteNugetSign + FolderPath: bin\net10.0 + signConfigType: inlineSignParams + inlineOperation: | + [ + { + "KeyCode": "CP-230012", + "OperationCode": "SigntoolSign", + "Parameters": { + "OpusName": "Microsoft.Coyote", + "OpusInfo": "https://github.com/Microsoft/Coyote", + "FileDigest": "/fd \"SHA256\"", + "PageHash": "/PH", + "TimeStamp": "/tr \"http://rfc3161.gtm.corp.microsoft.com/TSS/HttpTspServer\" /td sha256" + }, + "ToolName": "sign", + "ToolVersion": "1.0" + }, + { + "KeyCode": "CP-230012", + "OperationCode": "SigntoolVerify", + "Parameters": {}, + "ToolName": "sign", + "ToolVersion": "1.0" + } + ] + - task: EsrpCodeSigning@2 displayName: 'ESRP CodeSigning .NET 8.0' inputs: diff --git a/Scripts/build.ps1 b/Scripts/build.ps1 index e1bdc4cd7..960f288b4 100644 --- a/Scripts/build.ps1 +++ b/Scripts/build.ps1 @@ -51,7 +51,7 @@ if ($ci.IsPresent) { Write-Comment -text "Using configuration '$configuration'." -color "magenta" $solution = Join-Path -Path $ScriptDir -ChildPath ".." -AdditionalChildPath "Coyote.sln" -$command = "build -c $configuration /p:Platform=""Any CPU"" $extra_frameworks $solution" +$command = "build -m:1 -c $configuration /p:Platform=""Any CPU"" $extra_frameworks $solution" $error_msg = "Failed to build Coyote" Invoke-ToolCommand -tool $dotnet -cmd $command -error_msg $error_msg diff --git a/Scripts/common.psm1 b/Scripts/common.psm1 index 6f40570c0..713f4ecae 100644 --- a/Scripts/common.psm1 +++ b/Scripts/common.psm1 @@ -23,7 +23,8 @@ function Invoke-CoyoteTool([String]$cmd, [String]$dotnet, [String]$framework, [S $command = "$coyote $cmd $target" } - if ($command -eq "rewrite" -and $framework -ne "net6.0" -and $framework -ne "net8.0" -and $IsWindows) { + if ($cmd -eq "rewrite" -and $framework -ne "net10.0" -and $framework -ne "net8.0" -and + $framework -ne "net6.0" -and $IsWindows) { # NOTE: Mono.Cecil cannot sign assemblies on unix platforms. $command = "$command -snk $key" } @@ -156,11 +157,14 @@ function FindDotNetSdkVersion([String]$dotnet_sdk_path) { } # Finds the dotnet runtime version. -function FindDotNetRuntimeVersion([String]$dotnet_runtime_path) { - $globalJson = Join-Path -Path $PSScriptRoot -ChildPath ".." -AdditionalChildPath @("global.json") - $json = Get-Content $globalJson | Out-String | ConvertFrom-Json - $global_version = $json.sdk.version - return FindMatchingVersion -path $dotnet_runtime_path -version $global_version +function FindDotNetRuntimeVersion([String]$dotnet_runtime_path, [version]$version) { + if ($null -eq $version) { + $globalJson = Join-Path -Path $PSScriptRoot -ChildPath ".." -AdditionalChildPath @("global.json") + $json = Get-Content $globalJson | Out-String | ConvertFrom-Json + $version = $json.sdk.version + } + + return FindMatchingVersion -path $dotnet_runtime_path -version $version } # Searches the specified directory for the closest match for the given version. diff --git a/Scripts/gen-docs.ps1 b/Scripts/gen-docs.ps1 index 271f8f3fa..5ea2a08ea 100644 --- a/Scripts/gen-docs.ps1 +++ b/Scripts/gen-docs.ps1 @@ -3,7 +3,7 @@ $root_dir = "$PSScriptRoot\.." $packages_path = "$root_dir\packages" -$framework = "net8.0" +$framework = "net10.0" Import-Module $PSScriptRoot\common.psm1 -Force diff --git a/Scripts/run-benchmark-history.ps1 b/Scripts/run-benchmark-history.ps1 index d4717ad32..4d4c6e8d4 100644 --- a/Scripts/run-benchmark-history.ps1 +++ b/Scripts/run-benchmark-history.ps1 @@ -41,7 +41,7 @@ function RestoreBenchmark() { Invoke-Expression "sed -i 's/\\Performance.Tests.csproj/\\Microsoft.Coyote.Performance.Tests.csproj/' $RootDir\Coyote.sln" } -$benchmarks_dir = "$RootDir/Tools/BenchmarkRunner/bin/net8.0" +$benchmarks_dir = "$RootDir/Tools/BenchmarkRunner/bin/net10.0" $benchmark_runner = "BenchmarkRunner.exe" $index = 0 diff --git a/Scripts/run-benchmarks.ps1 b/Scripts/run-benchmarks.ps1 index f3e2cc786..eb11babaf 100644 --- a/Scripts/run-benchmarks.ps1 +++ b/Scripts/run-benchmarks.ps1 @@ -30,7 +30,7 @@ if ($local -eq ""){ } $current_dir = (Get-Item -Path "./").FullName -$benchmarks_dir = "$PSScriptRoot/../Tools/BenchmarkRunner/bin/net8.0" +$benchmarks_dir = "$PSScriptRoot/../Tools/BenchmarkRunner/bin/net10.0" $benchmark_runner = "BenchmarkRunner.exe" $artifacts_dir = "$current_dir/benchmark_$commit" diff --git a/Scripts/run-tests.ps1 b/Scripts/run-tests.ps1 index 0860364ba..488074784 100644 --- a/Scripts/run-tests.ps1 +++ b/Scripts/run-tests.ps1 @@ -2,8 +2,8 @@ # Licensed under the MIT License. param( - [ValidateSet("net8.0", "net6.0", "net462")] - [string]$framework = "net8.0", + [ValidateSet("net10.0", "net8.0", "net6.0", "net462")] + [string]$framework = "net10.0", [ValidateSet("all", "runtime", "rewriting", "testing", "actors", "actors-testing", "tools")] [string]$test = "all", [string]$filter = "", @@ -30,17 +30,14 @@ $targets = [ordered]@{ $dotnet = "dotnet" $dotnet_runtime_path = FindDotNetRuntimePath -dotnet $dotnet -runtime "NETCore" $aspnet_runtime_path = FindDotNetRuntimePath -dotnet $dotnet -runtime "AspNetCore" -$runtime_version = FindDotNetRuntimeVersion -dotnet_runtime_path $dotnet_runtime_path # NOTE: we do some hacks to get around a known issue with dotnet tool # command being available after locally being restored. # Example: https://github.com/dotnet/sdk/issues/11820 # Restore the local ilverify tool. -&dotnet nuget locals all --clear &dotnet tool restore -&dotnet tool install dotnet-ilverify --version 8.0.0 &dotnet tool list -$ilverify = "dotnet ilverify" +$ilverify = "dotnet tool run ilverify" [System.Environment]::SetEnvironmentVariable('COYOTE_CLI_TELEMETRY_OPTOUT', '1') @@ -59,14 +56,21 @@ foreach ($kvp in $targets.GetEnumerator()) { } $target = "$PSScriptRoot/../Tests/$($kvp.Value)/$($kvp.Value).csproj" - if ($f -eq "net8.0") { + if ($f -eq "net10.0" -or $f -eq "net8.0") { + $runtime_version = FindDotNetRuntimeVersion -dotnet_runtime_path $dotnet_runtime_path ` + -version $f.Substring(3) $AssemblyName = GetAssemblyName($target) - $command = [IO.Path]::Combine($PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net8.0", "$AssemblyName.dll") + $command = [IO.Path]::Combine($PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", $f, "$AssemblyName.dll") $command = $command + ' -r "' + [IO.Path]::Combine( ` - $PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net8.0", "*.dll") + '"' - $command = $command + ' -r "' + [IO.Path]::Combine($PSScriptRoot, "..", "bin", "net8.0", "*.dll") + '"' + $PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", $f, "*.dll") + '"' + $command = $command + ' -r "' + [IO.Path]::Combine($PSScriptRoot, "..", "bin", $f, "*.dll") + '"' $command = $command + ' -r "' + [IO.Path]::Combine($dotnet_runtime_path, $runtime_version, "*.dll") + '"' $command = $command + ' -r "' + [IO.Path]::Combine($aspnet_runtime_path, $runtime_version, "*.dll") + '"' + if ($f -eq "net10.0") { + # ILVerify rejects the SDK-generated inline-array span helper even before rewriting. + $command = $command + ' -e ".*InlineArrayAsReadOnlySpan.*"' + } + Invoke-ToolCommand -tool $ilverify -cmd $command -error_msg "found corrupted assembly rewriting" } diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 9e601edca..4dcda8cc4 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -13,7 +13,7 @@ - + \ No newline at end of file diff --git a/Source/Test/Rewriting/AssemblyInfo.cs b/Source/Test/Rewriting/AssemblyInfo.cs index c7ddf31f4..ebeb949a7 100644 --- a/Source/Test/Rewriting/AssemblyInfo.cs +++ b/Source/Test/Rewriting/AssemblyInfo.cs @@ -6,6 +6,7 @@ using System.IO; using System.Linq; using System.Reflection; +using Microsoft.Coyote.Runtime; using Mono.Cecil; using Mono.Cecil.Cil; @@ -280,6 +281,11 @@ private CustomAttribute GetCustomAttribute(Type attributeType) => /// private void ValidateAssembly() { + // Rewriting resolves the replacement types of the running Coyote host, so the host and + // the assembly must target the same .NET major version. This also covers any dependency + // that was loaded transitively, as such a dependency is rewritten as well. + TargetRuntimeValidator.ValidateRewritingTarget(this.FilePath, this.Definition); + if (this.IsAssemblyRewritten(out string version, out string signatureHash)) { // The assembly has been already rewritten so check if the signatures match. diff --git a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs index c169a91ae..095d7604c 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs +++ b/Source/Test/Rewriting/Passes/Rewriting/Types/TypeRewritingPass.cs @@ -88,6 +88,10 @@ internal TypeRewritingPass(RewritingOptions options, IEnumerable v this.KnownTypes[NameCache.ManualResetEvent] = typeof(Types.Threading.ManualResetEvent); this.KnownTypes[NameCache.EventWaitHandle] = typeof(Types.Threading.EventWaitHandle); this.KnownTypes[NameCache.WaitHandle] = typeof(Types.Threading.WaitHandle); +#if NET10_0_OR_GREATER + this.KnownTypes[NameCache.Lock] = typeof(Types.Threading.Lock); + this.KnownTypes[NameCache.LockScope] = typeof(Types.Threading.Lock.Scope); +#endif #if NET // Populate the map with the known HTTP and web-related types. diff --git a/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs b/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs index 463bd5f49..6df089b8b 100644 --- a/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs +++ b/Source/Test/Rewriting/Passes/Rewriting/UncontrolledInvocationRewritingPass.cs @@ -156,6 +156,8 @@ member.Name is nameof(System.Threading.EventWaitHandle.TryOpenExisting))) return true; } else if (type.Name is nameof(System.Threading.ExecutionContext) || + type.Name is nameof(System.Threading.Barrier) || + type.Name is nameof(System.Threading.CountdownEvent) || type.Name is nameof(System.Threading.ManualResetEventSlim) || type.Name is nameof(System.Threading.Mutex) || type.Name is nameof(System.Threading.ReaderWriterLock) || diff --git a/Source/Test/Rewriting/RewritingEngine.cs b/Source/Test/Rewriting/RewritingEngine.cs index 36315033b..770555294 100644 --- a/Source/Test/Rewriting/RewritingEngine.cs +++ b/Source/Test/Rewriting/RewritingEngine.cs @@ -91,6 +91,14 @@ internal static void Run(RewritingOptions options, Configuration configuration, /// private void Run() { + // Validate that the runtime of the Coyote host is compatible with each requested target + // assembly before creating or modifying any output. Rewriting an assembly that targets a + // different .NET major version injects runtime references that the assembly cannot load. + foreach (string assemblyPath in this.Options.AssemblyPaths) + { + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath); + } + this.Profiler.StartMeasuringExecutionTime(); // Create the output directory and copy any necessary files. diff --git a/Source/Test/Rewriting/RewritingOptions.cs b/Source/Test/Rewriting/RewritingOptions.cs index c1ae70468..b6d574f8c 100644 --- a/Source/Test/Rewriting/RewritingOptions.cs +++ b/Source/Test/Rewriting/RewritingOptions.cs @@ -308,7 +308,8 @@ private static bool TryResolveTargetFramework(Assembly assembly, out string reso { if (tokens[0] == ".NETCoreApp") { - resolvedTargetFramework = tokens[1] is "v8.0" ? "net8.0" : + resolvedTargetFramework = tokens[1] is "v10.0" ? "net10.0" : + tokens[1] is "v8.0" ? "net8.0" : tokens[1] is "v6.0" ? "net6.0" : resolvedTargetFramework; } diff --git a/Source/Test/Rewriting/Types/NameCache.cs b/Source/Test/Rewriting/Types/NameCache.cs index 1e7be6d59..ee0659239 100644 --- a/Source/Test/Rewriting/Types/NameCache.cs +++ b/Source/Test/Rewriting/Types/NameCache.cs @@ -79,6 +79,10 @@ internal static class NameCache internal static string ManualResetEvent { get; } = typeof(SystemThreading.ManualResetEvent).FullName; internal static string EventWaitHandle { get; } = typeof(SystemThreading.EventWaitHandle).FullName; internal static string WaitHandle { get; } = typeof(SystemThreading.WaitHandle).FullName; +#if NET10_0_OR_GREATER + internal static string Lock { get; } = typeof(SystemThreading.Lock).FullName; + internal static string LockScope { get; } = typeof(SystemThreading.Lock).FullName + "/Scope"; +#endif internal static string GenericList { get; } = typeof(SystemGenericCollections.List<>).FullName; internal static string GenericDictionary { get; } = typeof(SystemGenericCollections.Dictionary<,>).FullName; diff --git a/Source/Test/Rewriting/Types/Threading/Lock.cs b/Source/Test/Rewriting/Types/Threading/Lock.cs new file mode 100644 index 000000000..bb66d73c4 --- /dev/null +++ b/Source/Test/Rewriting/Types/Threading/Lock.cs @@ -0,0 +1,183 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET10_0_OR_GREATER +using System; +using Microsoft.Coyote.Runtime; +using SystemLock = System.Threading.Lock; +using SystemSynchronizationLockException = System.Threading.SynchronizationLockException; + +#pragma warning disable CS9216 // The conversion preserves Lock identity for controlled synchronization. +namespace Microsoft.Coyote.Rewriting.Types.Threading +{ + /// + /// Provides methods for locks that can be controlled during testing. + /// + /// This type is intended for compiler use rather than use directly in code. + [System.ComponentModel.EditorBrowsable(System.ComponentModel.EditorBrowsableState.Never)] + public static class Lock + { + /// + /// Scope that releases a controlled lock when disposed. + /// + public ref struct Scope + { + private SystemLock Instance; + + internal Scope(SystemLock instance) + { + this.Instance = instance; + } + + /// + /// Releases the lock. + /// + public void Dispose() + { + SystemLock instance = this.Instance; + if (instance != null) + { + this.Instance = null; + Exit(instance); + } + } + } + + /// + /// Gets a value that indicates whether the current controlled operation holds the lock. + /// +#pragma warning disable CA1707 // Identifiers should not contain underscores +#pragma warning disable SA1300 // Element should begin with upper-case letter +#pragma warning disable IDE1006 // Naming Styles + public static bool get_IsHeldByCurrentThread(SystemLock instance) +#pragma warning restore IDE1006 // Naming Styles +#pragma warning restore SA1300 // Element should begin with upper-case letter +#pragma warning restore CA1707 // Identifiers should not contain underscores + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + var block = Monitor.SynchronizedBlock.Find(instance); + return block != null && block.IsEntered(); + } + + return instance.IsHeldByCurrentThread; + } + + /// + /// Acquires the lock. + /// + public static void Enter(SystemLock instance) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + Monitor.SynchronizedBlock.Lock(instance); + } + else + { + DelayOperation(runtime); + instance.Enter(); + } + } + + /// + /// Acquires the lock and returns a scope that releases it when disposed. + /// + public static Scope EnterScope(SystemLock instance) + { + Enter(instance); + return new Scope(instance); + } + + /// + /// Tries to acquire the lock without blocking. + /// + public static bool TryEnter(SystemLock instance) => TryEnter(instance, 0); + + /// + /// Tries to acquire the lock within the specified timeout. + /// + public static bool TryEnter(SystemLock instance, int millisecondsTimeout) + { + if (millisecondsTimeout < -1) + { + throw new ArgumentOutOfRangeException(nameof(millisecondsTimeout)); + } + + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + if (Monitor.SynchronizedBlock.TryLock(instance)) + { + return true; + } + + if (millisecondsTimeout is 0) + { + return false; + } + + if (millisecondsTimeout > 0) + { + runtime.NotifyAssertionFailure( + "Invoking 'Lock.TryEnter' with a finite timeout is not supported in systematic testing."); + return false; + } + + Monitor.SynchronizedBlock.Lock(instance); + return true; + } + + DelayOperation(runtime); + return instance.TryEnter(millisecondsTimeout); + } + + /// + /// Tries to acquire the lock within the specified timeout. + /// + public static bool TryEnter(SystemLock instance, TimeSpan timeout) + { + long totalMilliseconds = (long)timeout.TotalMilliseconds; + if (totalMilliseconds < -1 || totalMilliseconds > int.MaxValue) + { + throw new ArgumentOutOfRangeException(nameof(timeout)); + } + + return TryEnter(instance, (int)totalMilliseconds); + } + + /// + /// Releases the lock. + /// + public static void Exit(SystemLock instance) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + var block = Monitor.SynchronizedBlock.Find(instance); + if (block is null || !block.IsEntered()) + { + throw new SystemSynchronizationLockException(); + } + + block.Exit(); + } + else + { + instance.Exit(); + } + } + + private static void DelayOperation(CoyoteRuntime runtime) + { + if (runtime.SchedulingPolicy is SchedulingPolicy.Fuzzing && + runtime.TryGetExecutingOperation(out ControlledOperation current)) + { + runtime.DelayOperation(current); + } + } + } +} +#pragma warning restore CS9216 // The conversion preserves Lock identity for controlled synchronization. +#endif diff --git a/Source/Test/Rewriting/Types/Threading/Monitor.cs b/Source/Test/Rewriting/Types/Threading/Monitor.cs index bab1dd3bf..890dbca7a 100644 --- a/Source/Test/Rewriting/Types/Threading/Monitor.cs +++ b/Source/Test/Rewriting/Types/Threading/Monitor.cs @@ -437,6 +437,13 @@ internal static SynchronizedBlock Lock(object syncObject) => Cache.GetOrAdd(syncObject, key => new Lazy( () => new SynchronizedBlock(CoyoteRuntime.Current, key))).Value.EnterLock(); + /// + /// Tries to enter the lock associated with the specified synchronization object. + /// + internal static bool TryLock(object syncObject) => + Cache.GetOrAdd(syncObject, key => new Lazy( + () => new SynchronizedBlock(CoyoteRuntime.Current, key))).Value.TryEnterLock(); + /// /// Finds the synchronized block associated with the specified synchronization object. /// @@ -506,6 +513,47 @@ private SynchronizedBlock EnterLock() return this; } + /// + /// Tries to enter the lock without blocking. + /// + private bool TryEnterLock() + { + CoyoteRuntime runtime = this.GetRuntime(); + var op = runtime.GetExecutingOperation(); + if (this.Owner != null && this.Owner != op) + { + return false; + } + + // Reference count this access before reaching any scheduling point, else another operation + // can enter and exit this lock in the meantime, which would remove this instance from the + // cache and orphan the lock that this operation is about to acquire. + SystemInterlocked.Increment(ref this.UseCount); + if (runtime.Configuration.IsLockAccessRaceCheckingEnabled && this.Owner is null) + { + // If this operation is trying to acquire this lock while it is free, then inject a scheduling + // point to give another enabled operation the chance to race and acquire this lock. + runtime.ScheduleNextOperation(default, SchedulingPointType.Acquire); + if (this.Owner != null && this.Owner != op) + { + this.ReleaseUse(); + return false; + } + } + + if (this.Owner == op) + { + this.LockCountMap[op]++; + } + else + { + this.Owner = op; + this.LockCountMap.Add(op, 1); + } + + return true; + } + /// /// Notifies a thread in the waiting queue of a change in the locked object's state. /// @@ -686,8 +734,19 @@ internal void Exit() this.UnlockNextReady(); } + this.ReleaseUse(); + } + + /// + /// Releases an access to this synchronized block, removing it from the cache + /// if it is no longer being accessed. + /// + private void ReleaseUse() + { int useCount = SystemInterlocked.Decrement(ref this.UseCount); - if (useCount is 0 && Cache[this.SyncObject].Value == this) + if (useCount is 0 && + Cache.TryGetValue(this.SyncObject, out Lazy lazyBlock) && + lazyBlock.Value == this) { // It is safe to remove this instance from the cache. Cache.TryRemove(this.SyncObject, out _); diff --git a/Source/Test/Rewriting/Types/Threading/Tasks/Task.cs b/Source/Test/Rewriting/Types/Threading/Tasks/Task.cs index 2db9b614a..bcfa65019 100644 --- a/Source/Test/Rewriting/Types/Threading/Tasks/Task.cs +++ b/Source/Test/Rewriting/Types/Threading/Tasks/Task.cs @@ -212,6 +212,168 @@ public static SystemTask Delay(TimeSpan delay, SystemCancellationToken cancellat return runtime.ScheduleDelay(delay, cancellationToken); } +#if NET8_0_OR_GREATER + /// + /// Creates a task that completes after a specified time interval. + /// + public static SystemTask Delay(TimeSpan delay, TimeProvider timeProvider) => + Delay(delay, timeProvider, default); + + /// + /// Creates a task that completes after a specified time interval. + /// + public static SystemTask Delay(TimeSpan delay, TimeProvider timeProvider, + SystemCancellationToken cancellationToken) + { + ArgumentNullException.ThrowIfNull(timeProvider); + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.None) + { + return SystemTask.Delay(delay, timeProvider, cancellationToken); + } + + if (!ReferenceEquals(timeProvider, TimeProvider.System)) + { + const string message = "Custom time providers are not supported in systematic testing."; + runtime.NotifyAssertionFailure(message); + return FromException(new NotSupportedException(message)); + } + + return runtime.ScheduleDelay(delay, cancellationToken); + } +#endif + +#if NET + /// + /// Waits asynchronously for the task to complete or for cancellation to be requested. + /// + public static SystemTask WaitAsync(SystemTask task, SystemCancellationToken cancellationToken) + { + SystemTask result = task.WaitAsync(cancellationToken); + CoyoteRuntime.Current.RegisterKnownControlledTask(result); + return result; + } + + /// + /// Waits asynchronously for the task to complete within the specified timeout. + /// + public static SystemTask WaitAsync(SystemTask task, TimeSpan timeout) => + WaitAsync(task, timeout, default(SystemCancellationToken)); + +#if NET8_0_OR_GREATER + /// + /// Waits asynchronously for the task to complete within the specified timeout. + /// + public static SystemTask WaitAsync(SystemTask task, TimeSpan timeout, TimeProvider timeProvider) => + WaitAsync(task, timeout, timeProvider, default); +#endif + + /// + /// Waits asynchronously for the task to complete within the specified timeout or for cancellation. + /// + public static SystemTask WaitAsync(SystemTask task, TimeSpan timeout, + SystemCancellationToken cancellationToken) + { + ValidateTimeout(timeout); + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.None) + { + return task.WaitAsync(timeout, cancellationToken); + } + + return WaitAsync(task, timeout, runtime, cancellationToken); + } + +#if NET8_0_OR_GREATER + /// + /// Waits asynchronously for the task to complete within the specified timeout or for cancellation. + /// + public static SystemTask WaitAsync(SystemTask task, TimeSpan timeout, TimeProvider timeProvider, + SystemCancellationToken cancellationToken) + { + ArgumentNullException.ThrowIfNull(timeProvider); + ValidateTimeout(timeout); + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.None) + { + return task.WaitAsync(timeout, timeProvider, cancellationToken); + } + + if (!ReferenceEquals(timeProvider, TimeProvider.System)) + { + const string message = "Custom time providers are not supported in systematic testing."; + runtime.NotifyAssertionFailure(message); + return FromException(new NotSupportedException(message)); + } + + return WaitAsync(task, timeout, runtime, cancellationToken); + } +#endif + + private static SystemTask WaitAsync(SystemTask task, TimeSpan timeout, + CoyoteRuntime runtime, SystemCancellationToken cancellationToken) + { + if (task.IsCompleted) + { + // An already completed task takes precedence over both cancellation and the + // timeout, which matches the uncontrolled semantics of this API. + runtime.RegisterKnownControlledTask(task); + return task; + } + + if (cancellationToken.IsCancellationRequested) + { + // An already canceled token deterministically takes precedence over the timeout, + // which matches the uncontrolled semantics of this API. + SystemTask canceled = SystemTask.FromCanceled(cancellationToken); + runtime.RegisterKnownControlledTask(canceled); + return canceled; + } + + if (timeout == System.Threading.Timeout.InfiniteTimeSpan) + { + return WaitAsync(task, cancellationToken); + } + + if ((long)timeout.TotalMilliseconds is 0) + { + // A zero timeout expires before the task is given any chance to complete, so it + // deterministically wins, which matches the uncontrolled semantics of this API. + return FromException(new TimeoutException()); + } + + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + // Systematic testing does not model the passage of wall-clock time, so a finite + // timeout must not be explored as an operation racing the task to complete the + // wait, else the wait times out spuriously in some schedules, no matter how large + // the timeout is. Instead, the wait is explored as if the timeout was infinite, + // which is how the runtime models the timeout of the other controlled wait APIs, + // such as 'Task.Wait', 'Task.WaitAll', 'Monitor.Wait' and 'SemaphoreSlim.Wait'. + // A wait that no operation can complete is then reported as a deadlock. + return WaitAsync(task, cancellationToken); + } + + // Systematic fuzzing executes the program in real time, so the timeout keeps its + // wall-clock meaning and is delegated to the uncontrolled runtime. + SystemTask result = task.WaitAsync(timeout, cancellationToken); + runtime.RegisterKnownControlledTask(result); + return result; + } + + private static void ValidateTimeout(TimeSpan timeout) + { + // Match Timer.MaxSupportedTimeout in .NET 8 and .NET 10. The runtime reserves + // uint.MaxValue for the -1 millisecond infinite-timeout sentinel. + const long MaxSupportedTimeoutMilliseconds = 0xfffffffe; + long totalMilliseconds = (long)timeout.TotalMilliseconds; + if (totalMilliseconds < -1 || totalMilliseconds > MaxSupportedTimeoutMilliseconds) + { + throw new ArgumentOutOfRangeException(nameof(timeout)); + } + } +#endif + /// /// Creates a task that will complete when all tasks in the specified array have completed. /// @@ -223,6 +385,96 @@ public static SystemTask WhenAll(params SystemTask[] tasks) return task; } +#if NET10_0_OR_GREATER + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable WhenEach(params SystemTask[] tasks) + { + ArgumentNullException.ThrowIfNull(tasks); + return WhenEach((ReadOnlySpan)tasks); + } + + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable WhenEach(params ReadOnlySpan tasks) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy != SchedulingPolicy.Interleaving) + { + return SystemTask.WhenEach(tasks); + } + + return WhenEachState.Iterate(WhenEachState.Create(runtime, tasks)); + } + + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable WhenEach(IEnumerable tasks) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy != SchedulingPolicy.Interleaving) + { + return SystemTask.WhenEach(tasks); + } + + return WhenEachState.Iterate(WhenEachState.Create(runtime, tasks)); + } + + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable> WhenEach( + params SystemTasks.Task[] tasks) + { + ArgumentNullException.ThrowIfNull(tasks); + return WhenEach((ReadOnlySpan>)tasks); + } + + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable> WhenEach( + params ReadOnlySpan> tasks) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy != SchedulingPolicy.Interleaving) + { + return SystemTask.WhenEach(tasks); + } + + return WhenEachState.Iterate>(WhenEachState.Create(runtime, tasks)); + } + + /// + /// Creates an asynchronous enumerable that yields tasks as they complete. + /// + public static IAsyncEnumerable> WhenEach( + IEnumerable> tasks) + { + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy != SchedulingPolicy.Interleaving) + { + return SystemTask.WhenEach(tasks); + } + + return WhenEachState.Iterate>(WhenEachState.Create(runtime, tasks)); + } + + /// + /// Creates a task that will complete when all tasks in the specified span have completed. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static SystemTask WhenAll(params ReadOnlySpan tasks) + { + SystemTask task = SystemTask.WhenAll(tasks); + CoyoteRuntime.Current.RegisterKnownControlledTask(task); + return task; + } +#endif + /// /// Creates a task that will complete when all tasks in the specified enumerable collection have completed. /// @@ -245,6 +497,20 @@ public static SystemTasks.Task WhenAll(params SystemTasks.Ta return task; } +#if NET10_0_OR_GREATER + /// + /// Creates a task that will complete when all tasks in the specified span have completed. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static SystemTasks.Task WhenAll( + params ReadOnlySpan> tasks) + { + SystemTasks.Task task = SystemTask.WhenAll(tasks); + CoyoteRuntime.Current.RegisterKnownControlledTask(task); + return task; + } +#endif + /// /// Creates a task that will complete when all tasks in the specified enumerable collection have completed. /// @@ -267,6 +533,19 @@ public static SystemTasks.Task WhenAny(params SystemTask[] tasks) return task; } +#if NET10_0_OR_GREATER + /// + /// Creates a task that will complete when any task in the specified span has completed. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static SystemTasks.Task WhenAny(params ReadOnlySpan tasks) + { + SystemTasks.Task task = SystemTask.WhenAny(tasks); + CoyoteRuntime.Current.RegisterKnownControlledTask(task); + return task; + } +#endif + /// /// Creates a task that will complete when any task in the specified enumerable collection have completed. /// @@ -315,6 +594,20 @@ public static SystemTasks.Task WhenAny(SystemTask task1, SystemTask return task; } +#if NET10_0_OR_GREATER + /// + /// Creates a task that will complete when any task in the specified span has completed. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static SystemTasks.Task> WhenAny( + params ReadOnlySpan> tasks) + { + SystemTasks.Task> task = SystemTask.WhenAny(tasks); + CoyoteRuntime.Current.RegisterKnownControlledTask(task); + return task; + } +#endif + /// /// Creates a task that will complete when any task in the specified /// enumerable collection have completed. @@ -335,6 +628,15 @@ public static SystemTasks.Task WhenAny(SystemTask task1, SystemTask public static void WaitAll(params SystemTask[] tasks) => WaitAll(tasks, SystemTimeout.Infinite, default); +#if NET10_0_OR_GREATER + /// + /// Waits for all of the provided task objects to complete execution. + /// + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static void WaitAll(params ReadOnlySpan tasks) => + WaitAll(tasks.ToArray(), SystemTimeout.Infinite, default); +#endif + /// /// Waits for all of the provided task objects to complete execution /// within a specified time interval. @@ -365,6 +667,18 @@ public static bool WaitAll(SystemTask[] tasks, int millisecondsTimeout) => public static void WaitAll(SystemTask[] tasks, SystemCancellationToken cancellationToken) => WaitAll(tasks, SystemTimeout.Infinite, cancellationToken); +#if NET10_0_OR_GREATER + /// + /// Waits for all tasks in the enumerable collection to complete unless the wait is canceled. + /// + public static void WaitAll(IEnumerable tasks, + SystemCancellationToken cancellationToken = default) + { + ArgumentNullException.ThrowIfNull(tasks); + WaitAll(new List(tasks).ToArray(), cancellationToken); + } +#endif + /// /// Waits for any of the provided task objects to complete execution within a specified /// number of milliseconds or until a cancellation token is cancelled. @@ -372,8 +686,23 @@ public static void WaitAll(SystemTask[] tasks, SystemCancellationToken cancellat public static bool WaitAll(SystemTask[] tasks, int millisecondsTimeout, SystemCancellationToken cancellationToken) { + if (tasks is null) + { + throw new ArgumentNullException(nameof(tasks)); + } + + for (int idx = 0; idx < tasks.Length; idx++) + { + if (tasks[idx] is null) + { + throw new ArgumentException("The tasks collection included a null task.", nameof(tasks)); + } + } + + cancellationToken.ThrowIfCancellationRequested(); + var runtime = CoyoteRuntime.Current; - if (runtime.SchedulingPolicy != SchedulingPolicy.None && tasks != null) + if (runtime.SchedulingPolicy != SchedulingPolicy.None) { // TODO: support timeouts during testing, this would become false if there is a timeout. TaskServices.WaitUntilAllTasksComplete(runtime, tasks); @@ -619,6 +948,144 @@ public static TaskAwaiter GetAwaiter(SystemTasks.Task task) => public static ConfiguredTaskAwaitable ConfigureAwait( SystemTasks.Task task, bool continueOnCapturedContext) => new ConfiguredTaskAwaitable(task, continueOnCapturedContext); + +#if NET + /// + /// Waits asynchronously for the task to complete or for cancellation to be requested. + /// + public static SystemTasks.Task WaitAsync(SystemTasks.Task task, + SystemCancellationToken cancellationToken) + { + SystemTasks.Task result = task.WaitAsync(cancellationToken); + CoyoteRuntime.Current.RegisterKnownControlledTask(result); + return result; + } + + /// + /// Waits asynchronously for the task to complete within the specified timeout. + /// + public static SystemTasks.Task WaitAsync(SystemTasks.Task task, TimeSpan timeout) => + WaitAsync(task, timeout, default(SystemCancellationToken)); + +#if NET8_0_OR_GREATER + /// + /// Waits asynchronously for the task to complete within the specified timeout. + /// + public static SystemTasks.Task WaitAsync(SystemTasks.Task task, TimeSpan timeout, + TimeProvider timeProvider) => + WaitAsync(task, timeout, timeProvider, default); +#endif + + /// + /// Waits asynchronously for the task to complete within the specified timeout or for cancellation. + /// + public static SystemTasks.Task WaitAsync(SystemTasks.Task task, TimeSpan timeout, + SystemCancellationToken cancellationToken) + { + const long MaxSupportedTimeoutMilliseconds = 0xfffffffe; + long totalMilliseconds = (long)timeout.TotalMilliseconds; + if (totalMilliseconds < -1 || totalMilliseconds > MaxSupportedTimeoutMilliseconds) + { + throw new ArgumentOutOfRangeException(nameof(timeout)); + } + + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.None) + { + return task.WaitAsync(timeout, cancellationToken); + } + + return WaitAsync(task, timeout, runtime, cancellationToken); + } + +#if NET8_0_OR_GREATER + /// + /// Waits asynchronously for the task to complete within the specified timeout or for cancellation. + /// + public static SystemTasks.Task WaitAsync(SystemTasks.Task task, TimeSpan timeout, + TimeProvider timeProvider, SystemCancellationToken cancellationToken) + { + ArgumentNullException.ThrowIfNull(timeProvider); + const long MaxSupportedTimeoutMilliseconds = 0xfffffffe; + long totalMilliseconds = (long)timeout.TotalMilliseconds; + if (totalMilliseconds < -1 || totalMilliseconds > MaxSupportedTimeoutMilliseconds) + { + throw new ArgumentOutOfRangeException(nameof(timeout)); + } + + var runtime = CoyoteRuntime.Current; + if (runtime.SchedulingPolicy is SchedulingPolicy.None) + { + return task.WaitAsync(timeout, timeProvider, cancellationToken); + } + + if (!ReferenceEquals(timeProvider, TimeProvider.System)) + { + const string message = "Custom time providers are not supported in systematic testing."; + runtime.NotifyAssertionFailure(message); + SystemTasks.Task unsupported = SystemTask.FromException( + new NotSupportedException(message)); + runtime.RegisterKnownControlledTask(unsupported); + return unsupported; + } + + return WaitAsync(task, timeout, runtime, cancellationToken); + } +#endif + + private static SystemTasks.Task WaitAsync(SystemTasks.Task task, TimeSpan timeout, + CoyoteRuntime runtime, SystemCancellationToken cancellationToken) + { + if (task.IsCompleted) + { + // An already completed task takes precedence over both cancellation and the + // timeout, which matches the uncontrolled semantics of this API. + runtime.RegisterKnownControlledTask(task); + return task; + } + + if (cancellationToken.IsCancellationRequested) + { + // An already canceled token deterministically takes precedence over the timeout, + // which matches the uncontrolled semantics of this API. + SystemTasks.Task canceled = SystemTask.FromCanceled(cancellationToken); + runtime.RegisterKnownControlledTask(canceled); + return canceled; + } + + if (timeout == System.Threading.Timeout.InfiniteTimeSpan) + { + return WaitAsync(task, cancellationToken); + } + + if ((long)timeout.TotalMilliseconds is 0) + { + // A zero timeout expires before the task is given any chance to complete, so it + // deterministically wins, which matches the uncontrolled semantics of this API. + SystemTasks.Task timedOut = SystemTask.FromException(new TimeoutException()); + runtime.RegisterKnownControlledTask(timedOut); + return timedOut; + } + + if (runtime.SchedulingPolicy is SchedulingPolicy.Interleaving) + { + // Systematic testing does not model the passage of wall-clock time, so a finite + // timeout must not be explored as an operation racing the task to complete the + // wait, else the wait times out spuriously in some schedules, no matter how large + // the timeout is. Instead, the wait is explored as if the timeout was infinite, + // which is how the runtime models the timeout of the other controlled wait APIs, + // such as 'Task.Wait', 'Task.WaitAll', 'Monitor.Wait' and 'SemaphoreSlim.Wait'. + // A wait that no operation can complete is then reported as a deadlock. + return WaitAsync(task, cancellationToken); + } + + // Systematic fuzzing executes the program in real time, so the timeout keeps its + // wall-clock meaning and is delegated to the uncontrolled runtime. + SystemTasks.Task result = task.WaitAsync(timeout, cancellationToken); + runtime.RegisterKnownControlledTask(result); + return result; + } +#endif #pragma warning restore CA1000 // Do not declare static members on generic types } } diff --git a/Source/Test/Rewriting/Types/Threading/Tasks/WhenEachState.cs b/Source/Test/Rewriting/Types/Threading/Tasks/WhenEachState.cs new file mode 100644 index 000000000..d1c6f095f --- /dev/null +++ b/Source/Test/Rewriting/Types/Threading/Tasks/WhenEachState.cs @@ -0,0 +1,224 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET10_0_OR_GREATER +using System; +using System.Collections.Generic; +using System.Threading; +using Microsoft.Coyote.Runtime; +using Microsoft.Coyote.Runtime.CompilerServices; +using SystemCancellationToken = System.Threading.CancellationToken; +using SystemEnumeratorCancellation = System.Runtime.CompilerServices.EnumeratorCancellationAttribute; +using SystemTask = System.Threading.Tasks.Task; + +namespace Microsoft.Coyote.Rewriting.Types.Threading.Tasks +{ + /// + /// Stores the state required to asynchronously enumerate a collection of tasks in the + /// order that they complete during systematic testing. + /// + /// + /// The uncontrolled methods signal the + /// enumeration from an uncontrolled thread pool thread, which the runtime is unable to + /// observe, so awaiting the enumeration can result in a false deadlock. The enumeration + /// is instead performed using controlled operations that pause until the next task + /// completes, which preserves the completion order of the enumerated tasks. + /// + internal sealed class WhenEachState + { + /// + /// Responsible for controlling the enumeration of the tasks. + /// + private readonly CoyoteRuntime Runtime; + + /// + /// Synchronizes access to the enumerated tasks. + /// + private readonly object SyncObject; + + /// + /// The tasks that have not completed yet, in the order that they were specified. + /// + private readonly List Pending; + + /// + /// The tasks that have completed, but have not been yielded yet, in completion order. + /// + private readonly Queue Completed; + + /// + /// Value 0 if this state has never been enumerated, else 1. + /// + private int Enumerated; + + /// + /// True if all tasks have been yielded, else false. + /// + private bool IsEnumerationCompleted + { + get + { + lock (this.SyncObject) + { + return this.Pending.Count is 0 && this.Completed.Count is 0; + } + } + } + + /// + /// Initializes a new instance of the class. + /// + private WhenEachState(CoyoteRuntime runtime) + { + this.Runtime = runtime; + this.SyncObject = new object(); + this.Pending = new List(); + this.Completed = new Queue(); + this.Enumerated = 0; + } + + /// + /// Creates the state for enumerating the specified tasks, or null if there are no tasks. + /// + internal static WhenEachState Create(CoyoteRuntime runtime, ReadOnlySpan tasks) + where TTask : SystemTask + { + WhenEachState state = null; + if (tasks.Length != 0) + { + state = new WhenEachState(runtime); + foreach (TTask task in tasks) + { + if (task is null) + { + throw new ArgumentException("The tasks argument included a null value.", nameof(tasks)); + } + + state.Pending.Add(task); + } + } + + return state; + } + + /// + /// Creates the state for enumerating the specified tasks, or null if there are no tasks. + /// + internal static WhenEachState Create(CoyoteRuntime runtime, IEnumerable tasks) + where TTask : SystemTask + { + ArgumentNullException.ThrowIfNull(tasks); + + WhenEachState state = null; + foreach (TTask task in tasks) + { + if (task is null) + { + throw new ArgumentException("The tasks argument included a null value.", nameof(tasks)); + } + + state ??= new WhenEachState(runtime); + state.Pending.Add(task); + } + + return state; + } + + /// + /// Asynchronously enumerates the tasks of the specified state as they complete. + /// + internal static async IAsyncEnumerable Iterate(WhenEachState state, + [SystemEnumeratorCancellation] SystemCancellationToken cancellationToken = default) + where TTask : SystemTask + { + // No matter how many times the enumerable is enumerated, each task is yielded only once, + // which is the same behavior as the uncontrolled 'Task.WhenEach' methods. + if (state?.TryStartEnumeration() is not true) + { + yield break; + } + + while (true) + { + if (state.TryDequeueCompletedTask(out SystemTask next)) + { + cancellationToken.ThrowIfCancellationRequested(); + yield return (TTask)next; + continue; + } + + if (state.IsEnumerationCompleted) + { + yield break; + } + + cancellationToken.ThrowIfCancellationRequested(); + + // Pause the current operation until the next task completes, or until cancellation is + // requested, so that the runtime remains in control of the asynchronous enumeration. + await AsyncConditionAwaiterStateMachine.RunAsync(state.Runtime, + () => state.HasCompletedTask() || cancellationToken.IsCancellationRequested, + debugMsg: "any of the enumerated tasks to complete"); + cancellationToken.ThrowIfCancellationRequested(); + } + } + + /// + /// Returns true if this state has not been enumerated before, else false. + /// + private bool TryStartEnumeration() => Interlocked.Exchange(ref this.Enumerated, 1) is 0; + + /// + /// Tries to dequeue the next task that completed, but has not been yielded yet. + /// + private bool TryDequeueCompletedTask(out SystemTask task) + { + lock (this.SyncObject) + { + this.CheckCompletedTasks(); + if (this.Completed.Count > 0) + { + task = this.Completed.Dequeue(); + return true; + } + } + + task = null; + return false; + } + + /// + /// Returns true if there is at least one task that completed, but has not been yielded yet. + /// + /// + /// The runtime invokes this each time that it checks if the paused enumeration can resume, + /// which captures the tasks in the order that they complete. + /// + private bool HasCompletedTask() + { + lock (this.SyncObject) + { + this.CheckCompletedTasks(); + return this.Completed.Count > 0; + } + } + + /// + /// Moves any tasks that completed since the previous check to the completed tasks. + /// + private void CheckCompletedTasks() + { + for (int idx = 0; idx < this.Pending.Count; idx++) + { + SystemTask task = this.Pending[idx]; + if (task.IsCompleted) + { + this.Completed.Enqueue(task); + this.Pending.RemoveAt(idx); + idx--; + } + } + } + } +} +#endif diff --git a/Source/Test/Runtime/TargetRuntimeValidator.cs b/Source/Test/Runtime/TargetRuntimeValidator.cs new file mode 100644 index 000000000..f4913a2f6 --- /dev/null +++ b/Source/Test/Runtime/TargetRuntimeValidator.cs @@ -0,0 +1,156 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Linq; +using System.Runtime.Versioning; +using Mono.Cecil; + +namespace Microsoft.Coyote.Runtime +{ + /// + /// Validates that the .NET runtime of the running Coyote host is compatible with the runtime + /// targeted by an assembly that Coyote is about to test or rewrite. + /// + internal static class TargetRuntimeValidator + { + /// + /// The full name of the attribute declaring the target framework of an assembly. + /// + private const string TargetFrameworkAttributeName = "System.Runtime.Versioning.TargetFrameworkAttribute"; + + /// + /// The framework identifier used by assemblies that target .NET (Core). + /// + private const string CoreFrameworkIdentifier = ".NETCoreApp"; + + /// + /// The .NET version of the running Coyote host, or null if the host is not running on .NET. + /// + private static readonly Version HostVersion = GetHostVersion(); + + /// + /// Validates that the running Coyote host can load the specified assembly for testing. + /// + /// + /// A host can load an assembly that targets an older .NET version, because the runtime rolls + /// forward, but it cannot load an assembly that targets a newer .NET version. + /// + internal static void ValidateTestingTarget(string assemblyPath) + { + using (AssemblyDefinition definition = AssemblyDefinition.ReadAssembly(assemblyPath)) + { + ValidateTestingTarget(assemblyPath, definition); + } + } + + /// + /// Validates that the running Coyote host can load the specified assembly for testing. + /// + internal static void ValidateTestingTarget(string assemblyPath, AssemblyDefinition definition) + { + FrameworkName framework = GetCoreTargetFramework(definition); + if (framework is null) + { + return; + } + + if (framework.Version > HostVersion) + { + throw new InvalidOperationException( + $"The Coyote host is running on .NET {HostVersion}, but test assembly " + + $"'{assemblyPath}' requires {framework.Identifier},Version=v{framework.Version}. " + + $"Run the net{framework.Version.Major}.0 Coyote host for this assembly."); + } + } + + /// + /// Validates that the running Coyote host can rewrite the specified assembly. + /// + /// + /// Rewriting resolves the replacement types of the running Coyote host, so the rewritten + /// assembly ends up referencing the runtime of that host. This is only safe when the host + /// and the assembly target the same .NET major version. + /// + internal static void ValidateRewritingTarget(string assemblyPath) + { + using (AssemblyDefinition definition = AssemblyDefinition.ReadAssembly(assemblyPath)) + { + ValidateRewritingTarget(assemblyPath, definition); + } + } + + /// + /// Validates that the running Coyote host can rewrite the specified assembly. + /// + internal static void ValidateRewritingTarget(string assemblyPath, AssemblyDefinition definition) + { + FrameworkName framework = GetCoreTargetFramework(definition); + if (framework is null) + { + return; + } + + if (framework.Version > HostVersion) + { + throw new InvalidOperationException( + $"The Coyote host is running on .NET {HostVersion}, but assembly '{assemblyPath}' " + + $"targets {framework.Identifier},Version=v{framework.Version}, which this host cannot " + + $"load. Run the net{framework.Version.Major}.0 Coyote host to rewrite this assembly."); + } + else if (framework.Version.Major < HostVersion.Major) + { + throw new InvalidOperationException( + $"The Coyote host is running on .NET {HostVersion}, but assembly '{assemblyPath}' " + + $"targets {framework.Identifier},Version=v{framework.Version}. Rewriting it with this " + + $"host would inject .NET {HostVersion} runtime references and the rewritten assembly " + + $"would fail to load on .NET {framework.Version}. Run the net{framework.Version.Major}.0 " + + "Coyote host to rewrite this assembly."); + } + } + + /// + /// Returns the .NET target framework of the specified assembly, or null if the assembly does + /// not declare a parsable .NET target framework, or if the host runtime is unknown. + /// + private static FrameworkName GetCoreTargetFramework(AssemblyDefinition definition) + { + if (HostVersion is null) + { + return null; + } + + CustomAttribute attribute = definition.CustomAttributes.FirstOrDefault( + candidate => candidate.AttributeType.FullName == TargetFrameworkAttributeName); + if (attribute is null || attribute.ConstructorArguments.Count != 1 || + !(attribute.ConstructorArguments[0].Value is string frameworkName)) + { + return null; + } + + FrameworkName framework; + try + { + framework = new FrameworkName(frameworkName); + } + catch (ArgumentException) + { + return null; + } + + return framework.Identifier == CoreFrameworkIdentifier ? framework : null; + } + + /// + /// Returns the .NET version of the running Coyote host, or null if the host is not running on .NET. + /// + private static Version GetHostVersion() + { +#if NET + return new Version(Environment.Version.Major, Environment.Version.Minor); +#else + return null; +#endif + } + } +} diff --git a/Source/Test/SystematicTesting/TestMethodInfo.cs b/Source/Test/SystematicTesting/TestMethodInfo.cs index 551751714..6c5a55929 100644 --- a/Source/Test/SystematicTesting/TestMethodInfo.cs +++ b/Source/Test/SystematicTesting/TestMethodInfo.cs @@ -102,6 +102,7 @@ private TestMethodInfo(Configuration configuration, LogWriter logWriter) { this.LogWriter = logWriter; #if NET + TargetRuntimeValidator.ValidateTestingTarget(configuration.AssemblyToBeAnalyzed); this.Assembly = AssemblyLoadContext.Default.LoadFromAssemblyPath(configuration.AssemblyToBeAnalyzed); this.LoadContext = AssemblyLoadContext.GetLoadContext(this.Assembly); this.DependencyContext = DependencyContext.Load(this.Assembly); diff --git a/Source/Test/Test.csproj b/Source/Test/Test.csproj index feb404383..9a85d9fba 100644 --- a/Source/Test/Test.csproj +++ b/Source/Test/Test.csproj @@ -22,6 +22,9 @@ + + + diff --git a/Tests/Compatibility/Net10Probe/CompatibilityProbe.cs b/Tests/Compatibility/Net10Probe/CompatibilityProbe.cs new file mode 100644 index 000000000..d2951a872 --- /dev/null +++ b/Tests/Compatibility/Net10Probe/CompatibilityProbe.cs @@ -0,0 +1,37 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using Microsoft.Coyote.SystematicTesting; +using Microsoft.Coyote.Specifications; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Coyote.Compatibility.Net10 +{ + public static class CompatibilityProbe + { + [Test] + public static async Task Execute() + { + var sync = new Lock(); + int count = 0; + Task first = Task.Run(() => + { + lock (sync) + { + count++; + } + }); + Task second = Task.Run(() => + { + lock (sync) + { + count++; + } + }); + + await Task.WhenAll(first, second); + Specification.Assert(count is 2, "Expected both tasks to execute."); + } + } +} diff --git a/Tests/Compatibility/Net10Probe/Net10Probe.csproj b/Tests/Compatibility/Net10Probe/Net10Probe.csproj new file mode 100644 index 000000000..4a2246ea0 --- /dev/null +++ b/Tests/Compatibility/Net10Probe/Net10Probe.csproj @@ -0,0 +1,18 @@ + + + net10.0 + 14.0 + enable + + + + ..\..\..\bin\net10.0\Microsoft.Coyote.dll + + + ..\..\..\bin\net10.0\Microsoft.Coyote.Actors.dll + + + ..\..\..\bin\net10.0\Microsoft.Coyote.Test.dll + + + diff --git a/Tests/Compatibility/Net10Probe/global.json b/Tests/Compatibility/Net10Probe/global.json new file mode 100644 index 000000000..195fae797 --- /dev/null +++ b/Tests/Compatibility/Net10Probe/global.json @@ -0,0 +1,6 @@ +{ + "sdk": { + "version": "10.0.303", + "rollForward": "latestPatch" + } +} diff --git a/Tests/Compatibility/Net8Probe/CompatibilityProbe.cs b/Tests/Compatibility/Net8Probe/CompatibilityProbe.cs new file mode 100644 index 000000000..97405504a --- /dev/null +++ b/Tests/Compatibility/Net8Probe/CompatibilityProbe.cs @@ -0,0 +1,36 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using Microsoft.Coyote.SystematicTesting; +using Microsoft.Coyote.Specifications; +using System.Threading.Tasks; + +namespace Microsoft.Coyote.Compatibility.Net8 +{ + public static class CompatibilityProbe + { + [Test] + public static async Task Execute() + { + object sync = new object(); + int count = 0; + Task first = Task.Run(() => + { + lock (sync) + { + count++; + } + }); + Task second = Task.Run(() => + { + lock (sync) + { + count++; + } + }); + + await Task.WhenAll(new[] { first, second }); + Specification.Assert(count is 2, "Expected both tasks to execute."); + } + } +} diff --git a/Tests/Compatibility/Net8Probe/Net8Probe.csproj b/Tests/Compatibility/Net8Probe/Net8Probe.csproj new file mode 100644 index 000000000..5407d8570 --- /dev/null +++ b/Tests/Compatibility/Net8Probe/Net8Probe.csproj @@ -0,0 +1,18 @@ + + + net8.0 + 12.0 + enable + + + + ..\..\..\bin\net8.0\Microsoft.Coyote.dll + + + ..\..\..\bin\net8.0\Microsoft.Coyote.Actors.dll + + + ..\..\..\bin\net8.0\Microsoft.Coyote.Test.dll + + + diff --git a/Tests/Compatibility/Net8Probe/global.json b/Tests/Compatibility/Net8Probe/global.json new file mode 100644 index 000000000..4a8c056fa --- /dev/null +++ b/Tests/Compatibility/Net8Probe/global.json @@ -0,0 +1,6 @@ +{ + "sdk": { + "version": "8.0.423", + "rollForward": "latestPatch" + } +} diff --git a/Tests/Compatibility/README.md b/Tests/Compatibility/README.md new file mode 100644 index 000000000..399054c9e --- /dev/null +++ b/Tests/Compatibility/README.md @@ -0,0 +1,135 @@ +# Runtime compatibility probes + +`Net8Probe` and `Net10Probe` exercise the native .NET 8 and .NET 10 Coyote +hosts. Each probe has its own `global.json`, so SDK sensitive commands must run +from the probe directory, and both the .NET 8 and the .NET 10 SDK must be +installed. + +## Running the matrix + +Build Coyote and then run the matrix from the repository root: + +```powershell +.\Scripts\build.ps1 +.\Tests\Compatibility\run-compatibility-matrix.ps1 +``` + +`run-compatibility-matrix.ps1` is the same command that the `Coyote CI` workflow +runs. It rebuilds each probe from scratch, copies that build into a workspace of +its own before every case, and fails if a host succeeds where it must fail, if +an expected diagnostic is missing, if a rejected command mutates the workspace, +or if a supported case does not execute the probe under Coyote control. Pass +`-nobuild` to reuse the existing probe builds. + +## The matrix + +| Host | Target | Expected | +| ---- | ------ | -------- | +| net8.0 | net8.0 probe | `rewrite` and `test` succeed | +| net10.0 | net10.0 probe | `rewrite` and `test` succeed | +| net10.0 | net8.0 probe rewritten by the net8.0 host | `test` succeeds, because the runtime rolls forward | +| net8.0 | net10.0 probe | `rewrite` and `test` are rejected | +| net10.0 | net8.0 probe | `rewrite` is rejected | + +The .NET 8 probe is built twice, once with the SDK pinned by its own +`global.json` and once with the SDK pinned by the `global.json` of the +repository root, and the matrix covers both builds. + +Never rewrite a probe inside its build directory. Coyote skips an assembly that +is already rewritten with a matching signature, so a second host invoked on that +same file reports success without doing anything, which is what previously made +this matrix look green. Copy the build of the probe into an empty directory +before each host invocation, exactly like the script does. + +## Reproducing a case by hand + +Every case below starts from a fresh copy of a probe build. On Linux and macOS +there is no `coyote.exe`, so invoke each host as `dotnet ./bin/net8.0/coyote.dll` +and `dotnet ./bin/net10.0/coyote.dll`, which is what the script does there too. +Build the probes first, from their own directory so that the pinned SDK is used: + +```powershell +Set-Location .\Tests\Compatibility\Net8Probe +dotnet build -c Release +Set-Location ..\Net10Probe +dotnet build -c Release +Set-Location ..\..\.. +``` + +The .NET 8 host rewrites and tests the .NET 8 probe: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net8-host -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net8Probe\bin\Release\net8.0\* -Destination .\Tests\Compatibility\bin\manual\net8-host -Recurse -Force +.\bin\net8.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net8-host\Net8Probe.dll +.\bin\net8.0\coyote.exe test .\Tests\Compatibility\bin\manual\net8-host\Net8Probe.dll -i 10 +``` + +The .NET 10 host tests the .NET 8 probe that the .NET 8 host rewrote, because +the .NET runtime rolls forward: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net10-host-net8-probe -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net8Probe\bin\Release\net8.0\* -Destination .\Tests\Compatibility\bin\manual\net10-host-net8-probe -Recurse -Force +.\bin\net8.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net10-host-net8-probe\Net8Probe.dll +.\bin\net10.0\coyote.exe test .\Tests\Compatibility\bin\manual\net10-host-net8-probe\Net8Probe.dll -i 10 +``` + +The .NET 10 host rewrites and tests the .NET 10 probe: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net10-host -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net10Probe\bin\Release\net10.0\* -Destination .\Tests\Compatibility\bin\manual\net10-host -Recurse -Force +.\bin\net10.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net10-host\Net10Probe.dll +.\bin\net10.0\coyote.exe test .\Tests\Compatibility\bin\manual\net10-host\Net10Probe.dll -i 10 +``` + +The .NET 10 host must reject the fresh .NET 8 probe, because rewriting it would +inject .NET 10 runtime references that the target cannot load, and it must leave +the assembly unchanged: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net10-host-rewrites-net8 -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net8Probe\bin\Release\net8.0\* -Destination .\Tests\Compatibility\bin\manual\net10-host-rewrites-net8 -Recurse -Force +.\bin\net10.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net10-host-rewrites-net8\Net8Probe.dll +``` + +```text +The Coyote host is running on .NET 10.0, but assembly '...\Net8Probe.dll' +targets .NETCoreApp,Version=v8.0. Rewriting it with this host would inject +.NET 10.0 runtime references and the rewritten assembly would fail to load on +.NET 8.0. Run the net8.0 Coyote host to rewrite this assembly. +``` + +The .NET 8 host must reject the fresh .NET 10 probe when rewriting it: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net8-host-rewrites-net10 -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net10Probe\bin\Release\net10.0\* -Destination .\Tests\Compatibility\bin\manual\net8-host-rewrites-net10 -Recurse -Force +.\bin\net8.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net8-host-rewrites-net10\Net10Probe.dll +``` + +```text +The Coyote host is running on .NET 8.0, but assembly '...\Net10Probe.dll' +targets .NETCoreApp,Version=v10.0, which this host cannot load. Run the net10.0 +Coyote host to rewrite this assembly. +``` + +The .NET 8 host must also reject the .NET 10 probe before reflection based test +discovery, and report both the host runtime and the required target runtime: + +```powershell +New-Item -Path .\Tests\Compatibility\bin\manual\net8-host-tests-net10 -ItemType Directory -Force +Copy-Item -Path .\Tests\Compatibility\Net10Probe\bin\Release\net10.0\* -Destination .\Tests\Compatibility\bin\manual\net8-host-tests-net10 -Recurse -Force +.\bin\net10.0\coyote.exe rewrite .\Tests\Compatibility\bin\manual\net8-host-tests-net10\Net10Probe.dll +.\bin\net8.0\coyote.exe test .\Tests\Compatibility\bin\manual\net8-host-tests-net10\Net10Probe.dll -i 10 +``` + +```text +The Coyote host is running on .NET 8.0, but test assembly '...\Net10Probe.dll' +requires .NETCoreApp,Version=v10.0. Run the net10.0 Coyote host for this +assembly. +``` + +Each rejected command exits with a non-zero exit code and leaves the target +assembly byte for byte unchanged. diff --git a/Tests/Compatibility/run-compatibility-matrix.ps1 b/Tests/Compatibility/run-compatibility-matrix.ps1 new file mode 100644 index 000000000..84fbb236c --- /dev/null +++ b/Tests/Compatibility/run-compatibility-matrix.ps1 @@ -0,0 +1,394 @@ +# Copyright (c) Microsoft Corporation. +# Licensed under the MIT License. + +# Runs the native .NET host compatibility matrix over the Coyote runtime compatibility probes. +# +# Every case copies a freshly built probe into an isolated workspace before it invokes a Coyote +# host, so that an assembly rewritten by an earlier case is never reused. Coyote skips an assembly +# that already carries a matching rewriting signature, which would otherwise hide the behavior that +# a case is meant to exercise. +# +# A supported pairing must rewrite the target and then execute it under Coyote control, while an +# unsupported pairing must fail with an actionable diagnostic and leave the workspace unchanged. + +param( + [ValidateSet("Release", "Debug")] + [string]$config = "Release", + [switch]$nobuild +) + +Import-Module $PSScriptRoot/../../Scripts/common.psm1 -Force + +CheckPSVersion + +[System.Environment]::SetEnvironmentVariable('COYOTE_CLI_TELEMETRY_OPTOUT', '1') + +$root_path = Join-Path -Path $PSScriptRoot -ChildPath ".." -AdditionalChildPath @("..") +$matrix_path = Join-Path -Path $PSScriptRoot -ChildPath "bin" -AdditionalChildPath @("matrix") +$iterations = 10 + +# The probes that the matrix rewrites and tests. The 'sdk' of a probe selects the SDK that builds +# it: 'probe' builds from the probe directory, which pins the SDK through the 'global.json' of the +# probe, and 'root' builds from the repository root, which pins the SDK of the root 'global.json'. +$probes = [ordered]@{ + "net8" = @{ + project = "Net8Probe" + assembly = "Net8Probe.dll" + output = "net8.0" + sdk = "probe" + } + "net8-sdk10" = @{ + project = "Net8Probe" + assembly = "Net8Probe.dll" + output = "net8.0-sdk10" + sdk = "root" + } + "net10" = @{ + project = "Net10Probe" + assembly = "Net10Probe.dll" + output = "net10.0" + sdk = "probe" + } +} + +# The host and target pairings covered by the matrix. Each case starts from a fresh copy of the +# specified probe, which the optional 'setup_framework' host rewrites, before the +# 'host_framework' host runs the asserted 'command'. +$cases = @( + @{ + name = "net8-host-rewrites-net8-probe" + probe = "net8" + host_framework = "net8.0" + command = "rewrite" + supported = $true + }, + @{ + name = "net8-host-tests-net8-probe" + probe = "net8" + setup_framework = "net8.0" + host_framework = "net8.0" + command = "test" + supported = $true + }, + @{ + # The .NET runtime rolls forward, so the net10.0 host must still test a net8.0 assembly + # that the net8.0 host rewrote. + name = "net10-host-tests-net8-probe" + probe = "net8" + setup_framework = "net8.0" + host_framework = "net10.0" + command = "test" + supported = $true + }, + @{ + name = "net8-host-rewrites-net8-probe-built-with-sdk10" + probe = "net8-sdk10" + host_framework = "net8.0" + command = "rewrite" + supported = $true + }, + @{ + name = "net8-host-tests-net8-probe-built-with-sdk10" + probe = "net8-sdk10" + setup_framework = "net8.0" + host_framework = "net8.0" + command = "test" + supported = $true + }, + @{ + name = "net10-host-rewrites-net10-probe" + probe = "net10" + host_framework = "net10.0" + command = "rewrite" + supported = $true + }, + @{ + name = "net10-host-tests-net10-probe" + probe = "net10" + setup_framework = "net10.0" + host_framework = "net10.0" + command = "test" + supported = $true + }, + @{ + name = "net8-host-rewrites-net10-probe" + probe = "net10" + host_framework = "net8.0" + command = "rewrite" + supported = $false + diagnostics = @( + "The Coyote host is running on .NET 8.0" + "targets .NETCoreApp,Version=v10.0" + "which this host cannot load" + "Run the net10.0 Coyote host to rewrite this assembly" + ) + }, + @{ + name = "net10-host-rewrites-net8-probe" + probe = "net8" + host_framework = "net10.0" + command = "rewrite" + supported = $false + diagnostics = @( + "The Coyote host is running on .NET 10.0" + "targets .NETCoreApp,Version=v8.0" + "would inject .NET 10.0 runtime references" + "Run the net8.0 Coyote host to rewrite this assembly" + ) + }, + @{ + name = "net10-host-rewrites-net8-probe-built-with-sdk10" + probe = "net8-sdk10" + host_framework = "net10.0" + command = "rewrite" + supported = $false + diagnostics = @( + "The Coyote host is running on .NET 10.0" + "targets .NETCoreApp,Version=v8.0" + "would inject .NET 10.0 runtime references" + "Run the net8.0 Coyote host to rewrite this assembly" + ) + }, + @{ + name = "net8-host-tests-net10-probe" + probe = "net10" + setup_framework = "net10.0" + host_framework = "net8.0" + command = "test" + supported = $false + diagnostics = @( + "The Coyote host is running on .NET 8.0" + "requires .NETCoreApp,Version=v10.0" + "Run the net10.0 Coyote host for this assembly" + ) + } +) + +# Builds the specified probe from scratch, so that the matrix never consumes a stale assembly. +# NOTE: a probe that pins its own SDK clears the whole build directory of its project, so it must +# be built before any probe of the same project that is built with the SDK of the repository root. +function Build-Probe($probe) { + $project_path = Join-Path -Path $PSScriptRoot -ChildPath $probe.project + $output_path = Join-Path -Path $project_path -ChildPath "bin" -AdditionalChildPath @($config, $probe.output) + Write-Comment -prefix "..." -text "Building the '$($probe.project)' probe into '$($probe.output)'" + if ($probe.sdk -eq "probe") { + Remove-Item -Path (Join-Path -Path $project_path -ChildPath "bin") -Recurse -Force -ErrorAction SilentlyContinue + Remove-Item -Path (Join-Path -Path $project_path -ChildPath "obj") -Recurse -Force -ErrorAction SilentlyContinue + + # Build from the probe directory so that the SDK pinned by its 'global.json' is used. + Push-Location $project_path + Invoke-ToolCommand -tool "dotnet" -cmd "build -c $config" ` + -error_msg "Failed to build the '$($probe.project)' probe" + Pop-Location + } else { + Remove-Item -Path $output_path -Recurse -Force -ErrorAction SilentlyContinue + + # Build from the repository root so that the SDK pinned by the root 'global.json' is used. + # The build is not incremental, else it can reuse the assembly compiled by the other SDK. + $project_file = Join-Path -Path $project_path -ChildPath "$($probe.project).csproj" + Push-Location $root_path + Invoke-ToolCommand -tool "dotnet" -cmd "build $project_file -c $config -o $output_path --no-incremental" ` + -error_msg "Failed to build the '$($probe.project)' probe with the SDK of the repository root" + Pop-Location + } +} + +# Creates an isolated workspace that contains a fresh copy of the specified probe build. +function New-Workspace([String]$case_name, $probe) { + $source_path = Join-Path -Path $PSScriptRoot -ChildPath $probe.project ` + -AdditionalChildPath @("bin", $config, $probe.output) + if (-not (Test-Path $source_path)) { + Write-Error "Unable to find the '$($probe.project)' probe build in '$source_path'." + exit 1 + } + + $workspace_path = Join-Path -Path $matrix_path -ChildPath $case_name + Remove-Item -Path $workspace_path -Recurse -Force -ErrorAction SilentlyContinue + New-Item -Path $workspace_path -ItemType Directory -Force | Out-Null + Copy-Item -Path (Join-Path -Path $source_path -ChildPath "*") -Destination $workspace_path -Recurse -Force + return $workspace_path +} + +# Invokes the Coyote host of the specified framework and returns its exit code and output. +function Invoke-CoyoteHost([String]$framework, [String]$command, [String]$target) { + $tool = Join-Path -Path $root_path -ChildPath "bin" -AdditionalChildPath @($framework, "coyote.exe") + $arguments = "$command $target" + if (-not (Test-Path $tool)) { + # NOTE: only Windows builds an executable host, so use the dotnet driver elsewhere. + $assembly = Join-Path -Path $root_path -ChildPath "bin" -AdditionalChildPath @($framework, "coyote.dll") + if (-not (Test-Path $assembly)) { + Write-Error "Unable to find the $framework Coyote host, build Coyote before running the matrix." + exit 1 + } + + $arguments = "$assembly $arguments" + $tool = "dotnet" + } + + if ($command -eq "test") { + $arguments = "$arguments -i $iterations" + } + + Write-Comment -prefix "....." -text "Invoking $tool $arguments" + $output = Invoke-Expression "$tool $arguments 2>&1 | Out-String" + return @{ exit_code = $LASTEXITCODE; output = [String]$output } +} + +# Returns true if the specified assembly carries a Coyote rewriting signature. The signature is an +# assembly level attribute, so the name of its type is in the metadata of a rewritten assembly. +function Test-RewritingSignature([String]$assembly_path) { + $bytes = [System.IO.File]::ReadAllBytes($assembly_path) + return [System.Text.Encoding]::Latin1.GetString($bytes).Contains("RewritingSignatureAttribute") +} + +# Returns the hash of every file in the specified directory, keyed by its relative path. +function Get-Snapshot([String]$directory) { + $snapshot = @{} + foreach ($file in Get-ChildItem -Path $directory -Recurse -File) { + $snapshot[$file.FullName.Substring($directory.Length)] = $(Get-FileHash $file.FullName).Hash + } + + return $snapshot +} + +# Returns how the specified directory snapshots differ. +function Compare-Snapshot($before, $after) { + $differences = @() + foreach ($path in $before.Keys) { + if (-not $after.ContainsKey($path)) { + $differences += "deleted '$path'" + } elseif ($after[$path] -ne $before[$path]) { + $differences += "modified '$path'" + } + } + + foreach ($path in $after.Keys) { + if (-not $before.ContainsKey($path)) { + $differences += "created '$path'" + } + } + + return , $differences +} + +# Records a failed expectation of the specified case. +function Assert-Expectation([String]$case_name, [bool]$condition, [String]$message) { + if (-not $condition) { + Write-Error "[$case_name] $message" + $script:failures += "[$case_name] $message" + } +} + +# Asserts that the specified host reported that it runs on the expected .NET version. +function Assert-Host([String]$case_name, [String]$framework, $result) { + $version = $framework.Substring(3).Split('.')[0] + Assert-Expectation $case_name $result.output.Contains("for .NET $version.") ` + "The $framework host did not report that it runs on .NET $version." +} + +$failures = @() + +Write-Comment -prefix "." -text "Running the native host compatibility matrix" -color "yellow" + +if ($nobuild.IsPresent) { + Write-Comment -prefix "..." -text "Reusing the existing probe builds" +} else { + foreach ($kvp in $probes.GetEnumerator()) { + Build-Probe -probe $($kvp.Value) + } +} + +foreach ($case in $cases) { + $expectation = if ($case.supported) { "supported" } else { "unsupported" } + Write-Comment -prefix ".." -text "Running the $expectation '$($case.name)' case" -color "yellow" + + $probe = $probes[$case.probe] + $workspace_path = New-Workspace -case_name $case.name -probe $probe + $target = Join-Path -Path $workspace_path -ChildPath $probe.assembly + + # A case that consumes an already rewritten assembly is not exercising its host, because + # Coyote skips any assembly that carries a matching rewriting signature. + if (Test-RewritingSignature $target) { + Assert-Expectation $case.name $false ` + "The '$($probe.project)' probe build is already rewritten, so the case is not exercised." + continue + } + + if ($case.setup_framework) { + $setup = Invoke-CoyoteHost -framework $case.setup_framework -command "rewrite" -target $target + if ($setup.exit_code -ne 0 -or -not (Test-RewritingSignature $target)) { + Write-Host $setup.output + Assert-Expectation $case.name $false ` + "The $($case.setup_framework) host failed to rewrite the '$($probe.project)' probe." + continue + } + } + + $before = Get-Snapshot $workspace_path + $result = Invoke-CoyoteHost -framework $case.host_framework -command $case.command -target $target + Write-Host $result.output + $after = Get-Snapshot $workspace_path + $differences = Compare-Snapshot -before $before -after $after + Assert-Host -case_name $case.name -framework $case.host_framework -result $result + + if (-not $case.supported) { + Assert-Expectation $case.name ($result.exit_code -ne 0) ` + "The $($case.host_framework) host unexpectedly succeeded to $($case.command) the target." + foreach ($diagnostic in $case.diagnostics) { + Assert-Expectation $case.name $result.output.Contains($diagnostic) ` + "The diagnostic of the $($case.host_framework) host is missing '$diagnostic'." + } + + # A rejected command must leave the target assembly, and any other file, untouched. + Assert-Expectation $case.name ($differences.Count -eq 0) ` + "The rejected command mutated the workspace: $($differences -join ', ')." + if ($case.command -eq "test") { + Assert-Expectation $case.name (-not $result.output.Contains("Iteration #1")) ` + "The $($case.host_framework) host ran the test instead of rejecting the target." + } + + continue + } + + Assert-Expectation $case.name ($result.exit_code -eq 0) ` + "The $($case.host_framework) host failed to $($case.command) the target with exit code $($result.exit_code)." + if ($case.command -eq "rewrite") { + Assert-Expectation $case.name ` + (-not $result.output.Contains("Skipping as assembly is already rewritten")) ` + "The $($case.host_framework) host skipped the target instead of rewriting it." + Assert-Expectation $case.name $result.output.Contains("Writing the modified") ` + "The $($case.host_framework) host did not write the rewritten target." + Assert-Expectation $case.name (Test-RewritingSignature $target) ` + "The rewritten target does not carry a rewriting signature." + Assert-Expectation $case.name ($differences -contains "modified '$([IO.Path]::DirectorySeparatorChar)$($probe.assembly)'") ` + "The rewritten target was not modified: $($differences -join ', ')." + } else { + Assert-Expectation $case.name (-not $result.output.Contains("Assembly is not rewritten for testing")) ` + "The $($case.host_framework) host tested an assembly that is not rewritten." + Assert-Expectation $case.name $result.output.Contains("Found 0 bugs.") ` + "The $($case.host_framework) host did not report a passing test." + Assert-Expectation $case.name $result.output.Contains("Explored $iterations execution paths") ` + "The $($case.host_framework) host did not explore $iterations execution paths." + + $controlled = [regex]::Match($result.output, "Controlled (\d+) operations") + Assert-Expectation $case.name ($controlled.Success -and [int]$controlled.Groups[1].Value -gt 0) ` + "The $($case.host_framework) host did not control any operation of the target." + Assert-Expectation $case.name (-not ($differences -contains "modified '$([IO.Path]::DirectorySeparatorChar)$($probe.assembly)'")) ` + "Testing the target modified it: $($differences -join ', ')." + } +} + +if ($failures.Count -gt 0) { + Write-Comment -prefix "." -text "The native host compatibility matrix found $($failures.Count) failures:" -color "red" + foreach ($failure in $failures) { + Write-Error $failure + } + + exit 1 +} + +Write-Comment -prefix "." -text "Done" -color "green" + +# NOTE: a rejected host command leaves a non-zero '$LASTEXITCODE' behind, which some CI shells +# report as a failure of the whole script. +exit 0 diff --git a/Tests/Tests.Actors.BugFinding/Tests.Actors.BugFinding.csproj b/Tests/Tests.Actors.BugFinding/Tests.Actors.BugFinding.csproj index 3ce2e9f5b..f5acf569f 100644 --- a/Tests/Tests.Actors.BugFinding/Tests.Actors.BugFinding.csproj +++ b/Tests/Tests.Actors.BugFinding/Tests.Actors.BugFinding.csproj @@ -7,7 +7,7 @@ false false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020,xUnit1030,xUnit1031 @@ -20,8 +20,8 @@ - - + + diff --git a/Tests/Tests.Actors/Tests.Actors.csproj b/Tests/Tests.Actors/Tests.Actors.csproj index f8d56fcec..2a1f525e3 100644 --- a/Tests/Tests.Actors/Tests.Actors.csproj +++ b/Tests/Tests.Actors/Tests.Actors.csproj @@ -7,7 +7,7 @@ false false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020,xUnit1030,xUnit1031 @@ -16,8 +16,8 @@ - - + + diff --git a/Tests/Tests.BugFinding/ConcurrencyFuzzing/Tasks/TaskWaitAsyncTests.cs b/Tests/Tests.BugFinding/ConcurrencyFuzzing/Tasks/TaskWaitAsyncTests.cs new file mode 100644 index 000000000..4920c3933 --- /dev/null +++ b/Tests/Tests.BugFinding/ConcurrencyFuzzing/Tasks/TaskWaitAsyncTests.cs @@ -0,0 +1,62 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET8_0_OR_GREATER +using System; +using System.Threading.Tasks; +using Microsoft.Coyote.Runtime; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.BugFinding.Tests.SystematicFuzzing +{ + public class TaskWaitAsyncTests : BaseBugFindingTest + { + public TaskWaitAsyncTests(ITestOutputHelper output) + : base(output) + { + } + + private protected override SchedulingPolicy SchedulingPolicy => SchedulingPolicy.Fuzzing; + + protected override Configuration GetConfiguration() + { + return base.GetConfiguration().WithSystematicFuzzingEnabled(); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithLongTimeoutAndConcurrentCompletion() + { + // Fuzzing executes in real time, so a timeout that cannot expire during the test + // must not be replaced by a fuzzed delay that expires immediately. + this.Test(async () => + { + var tcs = new TaskCompletionSource(); + Task producer = Task.Run(() => tcs.SetResult(true)); + await tcs.Task.WaitAsync(TimeSpan.FromMinutes(10)); + await producer; + + var resultTcs = new TaskCompletionSource(); + Task resultProducer = Task.Run(() => resultTcs.SetResult(7)); + Assert.Equal(7, await resultTcs.Task.WaitAsync(TimeSpan.FromMinutes(10), TimeProvider.System)); + await resultProducer; + }, + configuration: this.GetConfiguration().WithTestingIterations(50)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithZeroTimeoutAndIncompleteTask() + { + this.Test(async () => + { + var tcs = new TaskCompletionSource(); + await Assert.ThrowsAsync(() => tcs.Task.WaitAsync(TimeSpan.Zero)); + + var resultTcs = new TaskCompletionSource(); + await Assert.ThrowsAsync(() => resultTcs.Task.WaitAsync(TimeSpan.Zero)); + }, + configuration: this.GetConfiguration().WithTestingIterations(10)); + } + } +} +#endif diff --git a/Tests/Tests.BugFinding/Synchronization/MonitorTests.cs b/Tests/Tests.BugFinding/Synchronization/MonitorTests.cs index db4ad585c..13bd5d73e 100644 --- a/Tests/Tests.BugFinding/Synchronization/MonitorTests.cs +++ b/Tests/Tests.BugFinding/Synchronization/MonitorTests.cs @@ -6,6 +6,7 @@ using System.Diagnostics; using System.Threading; using System.Threading.Tasks; +using Microsoft.Coyote.Runtime; using Microsoft.Coyote.Specifications; using Xunit; using Xunit.Abstractions; @@ -154,6 +155,19 @@ public void TestMonitorWithInvalidUsage() replay: true); } + [Fact(Timeout = 5000)] + public void TestMonitorWithConcurrentTryLock() + { + this.Test(async () => + { + TryLockData data = new TryLockData(); + Task t1 = Task.Run(data.AcquireAndRelease); + Task t2 = Task.Run(data.AcquireAndRelease); + await Task.WhenAll(t1, t2); + }, + this.GetConfiguration().WithLockAccessRaceCheckingEnabled().WithTestingIterations(100)); + } + [Fact(Timeout = 5000)] public void TestComplexMonitor() { @@ -194,6 +208,33 @@ public void TestComplexMonitor() this.GetConfiguration()); } + private class TryLockData + { + private readonly object SyncObject; + private int EnteredCount; + + internal TryLockData() + { + this.SyncObject = new object(); + this.EnteredCount = 0; + } + + internal void AcquireAndRelease() + { + while (!SynchronizedBlock.TryLock(this.SyncObject)) + { + SchedulingPoint.Interleave(); + } + + this.EnteredCount++; + Specification.Assert(this.EnteredCount is 1, + "More than one operation acquired the lock, expected 1 but found {0}.", this.EnteredCount); + SchedulingPoint.Interleave(); + this.EnteredCount--; + Monitor.Exit(this.SyncObject); + } + } + private class SignalData { private readonly object SyncObject; diff --git a/Tests/Tests.BugFinding/Tasks/Join/TaskWaitAllTests.cs b/Tests/Tests.BugFinding/Tasks/Join/TaskWaitAllTests.cs index c39c58ca7..47cdaa65b 100644 --- a/Tests/Tests.BugFinding/Tasks/Join/TaskWaitAllTests.cs +++ b/Tests/Tests.BugFinding/Tasks/Join/TaskWaitAllTests.cs @@ -2,6 +2,7 @@ // Licensed under the MIT License. using System; +using System.Collections.Generic; using System.Threading; using System.Threading.Tasks; using Microsoft.Coyote.Specifications; @@ -237,5 +238,20 @@ public void TestWaitAllWithExceptionThrown() }, replay: true); } + +#if NET10_0_OR_GREATER + [Fact(Timeout = 5000)] + public void TestWaitAllEnumerableWithAlreadyCanceledToken() + { + this.TestWithException(() => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + IEnumerable tasks = new[] { new TaskCompletionSource().Task }; + Task.WaitAll(tasks, source.Token); + }, + replay: true); + } +#endif } } diff --git a/Tests/Tests.BugFinding/Tasks/Join/TaskWhenEachTests.cs b/Tests/Tests.BugFinding/Tasks/Join/TaskWhenEachTests.cs new file mode 100644 index 000000000..904d9a3d8 --- /dev/null +++ b/Tests/Tests.BugFinding/Tasks/Join/TaskWhenEachTests.cs @@ -0,0 +1,216 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET10_0_OR_GREATER +using System; +using System.Collections.Generic; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.Coyote.Specifications; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.BugFinding.Tests +{ + public class TaskWhenEachTests : BaseBugFindingTest + { + public TaskWhenEachTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestWhenEachWithTasksCompletedByAnotherOperation() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + + // Complete the tasks from another operation, which pauses the enumeration. + Task producer = Task.Run(async () => + { + await Task.Yield(); + first.SetResult(true); + await Task.Yield(); + second.SetResult(true); + }); + + var yielded = new List(); + await foreach (Task task in Task.WhenEach(first.Task, second.Task)) + { + Specification.Assert(task.IsCompleted, "Yielded a task that has not completed."); + yielded.Add(task); + } + + await producer; + Specification.Assert(yielded.Count is 2, "Yielded {0} tasks instead of 2.", yielded.Count); + Specification.Assert(ReferenceEquals(yielded[0], first.Task), "Yielded an unexpected first task."); + Specification.Assert(ReferenceEquals(yielded[1], second.Task), "Yielded an unexpected second task."); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachYieldsTasksInCompletionOrder() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + await using IAsyncEnumerator enumerator = + Task.WhenEach(first.Task, second.Task).GetAsyncEnumerator(); + + // Complete the tasks in the reverse order from other operations, which pauses + // the enumeration until each of the tasks completes. + Task completeSecond = Task.Run(() => second.SetResult(true)); + Specification.Assert(await enumerator.MoveNextAsync(), "The enumeration completed early."); + Specification.Assert(ReferenceEquals(enumerator.Current, second.Task), + "Yielded a task that is not the first task to complete."); + + Task completeFirst = Task.Run(() => first.SetResult(true)); + Specification.Assert(await enumerator.MoveNextAsync(), "The enumeration completed early."); + Specification.Assert(ReferenceEquals(enumerator.Current, first.Task), + "Yielded a task that is not the second task to complete."); + Specification.Assert(!await enumerator.MoveNextAsync(), "The enumeration did not complete."); + + await Task.WhenAll(completeSecond, completeFirst); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachWithGenericTasksCompletedByOtherOperations() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + + // Complete each task from a different operation, which pauses the enumeration. + Task completeFirst = Task.Run(() => first.SetResult(3)); + Task completeSecond = Task.Run(() => second.SetResult(5)); + + int count = 0; + int sum = 0; + await foreach (Task task in Task.WhenEach(first.Task, second.Task)) + { + Specification.Assert(task.IsCompleted, "Yielded a task that has not completed."); + count++; + sum += task.Result; + } + + await Task.WhenAll(completeFirst, completeSecond); + Specification.Assert(count is 2, "Yielded {0} tasks instead of 2.", count); + Specification.Assert(sum is 8, "Yielded results that sum to {0} instead of 8.", sum); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachWithEnumerableCompletedByOtherOperations() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + IEnumerable tasks = new List { first.Task, second.Task }; + + // Complete each task from a different operation, which pauses the enumeration. + Task completeFirst = Task.Run(() => first.SetResult(true)); + Task completeSecond = Task.Run(() => second.SetResult(true)); + + var yielded = new List(); + await foreach (Task task in Task.WhenEach(tasks)) + { + Specification.Assert(task.IsCompleted, "Yielded a task that has not completed."); + yielded.Add(task); + } + + await Task.WhenAll(completeFirst, completeSecond); + Specification.Assert(yielded.Count is 2, "Yielded {0} tasks instead of 2.", yielded.Count); + Specification.Assert(yielded.Contains(first.Task), "The first task was not yielded."); + Specification.Assert(yielded.Contains(second.Task), "The second task was not yielded."); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachStopsEnumerationEarlyWithPendingTask() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + Task completeFirst = Task.Run(() => first.SetResult(true)); + + int count = 0; + await foreach (Task task in Task.WhenEach(first.Task, second.Task)) + { + Specification.Assert(ReferenceEquals(task, first.Task), "Yielded an unexpected task."); + count++; + break; + } + + await completeFirst; + second.SetResult(true); + await second.Task; + Specification.Assert(count is 1, "Yielded {0} tasks instead of 1.", count); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachCancelledByAnotherOperation() + { + this.Test(async () => + { + var pending = new TaskCompletionSource(); + using var source = new CancellationTokenSource(); + await using IAsyncEnumerator enumerator = + Task.WhenEach(pending.Task).GetAsyncEnumerator(source.Token); + + // Cancel from another operation, which resumes the paused enumeration. + Task canceller = Task.Run(() => source.Cancel()); + + bool isCancelled = false; + try + { + await enumerator.MoveNextAsync(); + } + catch (OperationCanceledException) + { + isCancelled = true; + } + + Specification.Assert(isCancelled, "The enumeration was not cancelled."); + await canceller; + pending.SetResult(true); + await pending.Task; + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWhenEachDeadlock() + { + this.TestWithError(async () => + { + // Test that the enumeration deadlocks because one of the tasks cannot complete until later. + var tcs = new TaskCompletionSource(); + await foreach (Task task in Task.WhenEach(tcs.Task, Task.Delay(1))) + { + } + + tcs.SetResult(true); + await tcs.Task; + }, + errorChecker: (e) => + { + Assert.StartsWith("Deadlock detected.", e); + }, + replay: true); + } + } +} +#endif diff --git a/Tests/Tests.BugFinding/Tasks/TaskWaitAsyncTests.cs b/Tests/Tests.BugFinding/Tasks/TaskWaitAsyncTests.cs new file mode 100644 index 000000000..852e61d00 --- /dev/null +++ b/Tests/Tests.BugFinding/Tasks/TaskWaitAsyncTests.cs @@ -0,0 +1,486 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET8_0_OR_GREATER +using System; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.Coyote.Specifications; +using Microsoft.Coyote.Tests.Common.Tasks; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.BugFinding.Tests +{ + public class TaskWaitAsyncTests : BaseBugFindingTest + { + public TaskWaitAsyncTests(ITestOutputHelper output) + : base(output) + { + } + + private static readonly TimeSpan FiniteTimeout = TimeSpan.FromMilliseconds(10); + private static readonly TimeSpan LongTimeout = TimeSpan.FromMinutes(10); + private static readonly TimeSpan RuntimeSupportedLargeTimeout = TimeSpan.FromDays(30); + private static readonly TimeSpan InvalidTimeout = TimeSpan.FromMilliseconds(-2); + + [Fact(Timeout = 5000)] + public void TestWaitAsyncAcceptsRuntimeSupportedLargeTimeout() + { + using var uncontrolled = new CancellationTokenSource(); + string outcome = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreateCompletedTask(), RuntimeSupportedLargeTimeout, uncontrolled.Token); + string resultOutcome = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreateCompletedResultTask(), RuntimeSupportedLargeTimeout, uncontrolled.Token); + string timeProviderOutcome = WaitAsyncProvider.GetOutcomeWithTimeProvider( + WaitAsyncProvider.CreateCompletedTask(), RuntimeSupportedLargeTimeout, uncontrolled.Token); + string resultTimeProviderOutcome = WaitAsyncProvider.GetResultOutcomeWithTimeProvider( + WaitAsyncProvider.CreateCompletedResultTask(), RuntimeSupportedLargeTimeout, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.CompletedOutcome, outcome); + Assert.Equal(WaitAsyncProvider.GetCompletedOutcome(WaitAsyncProvider.ExpectedResult), resultOutcome); + Assert.Equal(WaitAsyncProvider.CompletedOutcome, timeProviderOutcome); + Assert.Equal(WaitAsyncProvider.GetCompletedOutcome(WaitAsyncProvider.ExpectedResult), + resultTimeProviderOutcome); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + await AssertOutcomeAsync(outcome, ct => + Task.CompletedTask.WaitAsync(RuntimeSupportedLargeTimeout, ct), source.Token); + await AssertResultOutcomeAsync(resultOutcome, ct => + Task.FromResult(WaitAsyncProvider.ExpectedResult).WaitAsync( + RuntimeSupportedLargeTimeout, ct), source.Token); + await AssertOutcomeAsync(timeProviderOutcome, ct => + Task.CompletedTask.WaitAsync(RuntimeSupportedLargeTimeout, TimeProvider.System, ct), + source.Token); + await AssertResultOutcomeAsync(resultTimeProviderOutcome, ct => + Task.FromResult(WaitAsyncProvider.ExpectedResult).WaitAsync( + RuntimeSupportedLargeTimeout, TimeProvider.System, ct), source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(1)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithAlreadyCanceledTokenAndIncompleteTask() + { + using var uncontrolled = new CancellationTokenSource(); + uncontrolled.Cancel(); + + // The uncontrolled overloads deterministically prefer cancellation over the timeout. + string zero = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), TimeSpan.Zero, uncontrolled.Token); + string finite = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), FiniteTimeout, uncontrolled.Token); + string infinite = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), Timeout.InfiniteTimeSpan, uncontrolled.Token); + string token = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), uncontrolled.Token); + string timeProvider = WaitAsyncProvider.GetOutcomeWithTimeProvider( + WaitAsyncProvider.CreatePendingTask(), TimeSpan.Zero, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, zero); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, finite); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, infinite); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, token); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, timeProvider); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + + await AssertOutcomeAsync(zero, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertOutcomeAsync(finite, ct => + new TaskCompletionSource().Task.WaitAsync(FiniteTimeout, ct), source.Token); + await AssertOutcomeAsync(infinite, ct => + new TaskCompletionSource().Task.WaitAsync(Timeout.InfiniteTimeSpan, ct), source.Token); + await AssertOutcomeAsync(token, ct => + new TaskCompletionSource().Task.WaitAsync(ct), source.Token); + await AssertOutcomeAsync(timeProvider, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, TimeProvider.System, ct), + source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithAlreadyCanceledTokenAndIncompleteGenericTask() + { + using var uncontrolled = new CancellationTokenSource(); + uncontrolled.Cancel(); + + string zero = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), TimeSpan.Zero, uncontrolled.Token); + string finite = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), FiniteTimeout, uncontrolled.Token); + string infinite = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), Timeout.InfiniteTimeSpan, uncontrolled.Token); + string token = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), uncontrolled.Token); + string timeProvider = WaitAsyncProvider.GetResultOutcomeWithTimeProvider( + WaitAsyncProvider.CreatePendingResultTask(), TimeSpan.Zero, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, zero); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, finite); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, infinite); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, token); + Assert.Equal(WaitAsyncProvider.WaitTokenCanceledOutcome, timeProvider); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + + await AssertResultOutcomeAsync(zero, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertResultOutcomeAsync(finite, ct => + new TaskCompletionSource().Task.WaitAsync(FiniteTimeout, ct), source.Token); + await AssertResultOutcomeAsync(infinite, ct => + new TaskCompletionSource().Task.WaitAsync(Timeout.InfiniteTimeSpan, ct), source.Token); + await AssertResultOutcomeAsync(token, ct => + new TaskCompletionSource().Task.WaitAsync(ct), source.Token); + await AssertResultOutcomeAsync(timeProvider, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, TimeProvider.System, ct), + source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithAlreadyCanceledTokenAndCompletedTask() + { + using var uncontrolled = new CancellationTokenSource(); + uncontrolled.Cancel(); + using var uncontrolledSource = new CancellationTokenSource(); + uncontrolledSource.Cancel(); + + // An already completed task takes precedence over the already canceled token. + string completed = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreateCompletedTask(), TimeSpan.Zero, uncontrolled.Token); + string faulted = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreateFaultedTask(), TimeSpan.Zero, uncontrolled.Token); + string canceled = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreateCanceledTask(uncontrolledSource.Token), TimeSpan.Zero, uncontrolled.Token); + string completedWithFiniteTimeout = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreateCompletedTask(), FiniteTimeout, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.CompletedOutcome, completed); + Assert.Equal($"fault({nameof(InvalidOperationException)})", faulted); + Assert.Equal(WaitAsyncProvider.SourceTokenCanceledOutcome, canceled); + Assert.Equal(WaitAsyncProvider.CompletedOutcome, completedWithFiniteTimeout); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + using var otherSource = new CancellationTokenSource(); + otherSource.Cancel(); + + await AssertOutcomeAsync(completed, ct => + Task.CompletedTask.WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertOutcomeAsync(faulted, ct => Task.FromException(new InvalidOperationException( + WaitAsyncProvider.ExpectedFaultMessage)).WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertOutcomeAsync(canceled, ct => + Task.FromCanceled(otherSource.Token).WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertOutcomeAsync(completedWithFiniteTimeout, ct => + Task.CompletedTask.WaitAsync(FiniteTimeout, ct), source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithAlreadyCanceledTokenAndCompletedGenericTask() + { + using var uncontrolled = new CancellationTokenSource(); + uncontrolled.Cancel(); + using var uncontrolledSource = new CancellationTokenSource(); + uncontrolledSource.Cancel(); + + string completed = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreateCompletedResultTask(), TimeSpan.Zero, uncontrolled.Token); + string faulted = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreateFaultedResultTask(), TimeSpan.Zero, uncontrolled.Token); + string canceled = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreateCanceledResultTask(uncontrolledSource.Token), TimeSpan.Zero, + uncontrolled.Token); + string completedWithFiniteTimeout = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreateCompletedResultTask(), FiniteTimeout, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.GetCompletedOutcome(WaitAsyncProvider.ExpectedResult), completed); + Assert.Equal($"fault({nameof(InvalidOperationException)})", faulted); + Assert.Equal(WaitAsyncProvider.SourceTokenCanceledOutcome, canceled); + Assert.Equal(WaitAsyncProvider.GetCompletedOutcome(WaitAsyncProvider.ExpectedResult), + completedWithFiniteTimeout); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + using var otherSource = new CancellationTokenSource(); + otherSource.Cancel(); + + await AssertResultOutcomeAsync(completed, ct => + Task.FromResult(WaitAsyncProvider.ExpectedResult).WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertResultOutcomeAsync(faulted, ct => Task.FromException( + new InvalidOperationException(WaitAsyncProvider.ExpectedFaultMessage)).WaitAsync( + TimeSpan.Zero, ct), source.Token); + await AssertResultOutcomeAsync(canceled, ct => + Task.FromCanceled(otherSource.Token).WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertResultOutcomeAsync(completedWithFiniteTimeout, ct => + Task.FromResult(WaitAsyncProvider.ExpectedResult).WaitAsync(FiniteTimeout, ct), source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncTimesOutWithUncanceledToken() + { + using var uncontrolled = new CancellationTokenSource(); + + // A token that is not canceled must not suppress the timeout. + string outcome = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), TimeSpan.Zero, uncontrolled.Token); + string resultOutcome = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), TimeSpan.Zero, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, outcome); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, resultOutcome); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + await AssertOutcomeAsync(outcome, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, ct), source.Token); + await AssertResultOutcomeAsync(resultOutcome, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, ct), source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncValidatesTimeoutBeforeCancellation() + { + using var uncontrolled = new CancellationTokenSource(); + uncontrolled.Cancel(); + + // The timeout is validated before the already canceled token is observed. + string outcome = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), InvalidTimeout, uncontrolled.Token); + string resultOutcome = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), InvalidTimeout, uncontrolled.Token); + Assert.Equal($"fault({nameof(ArgumentOutOfRangeException)})", outcome); + Assert.Equal($"fault({nameof(ArgumentOutOfRangeException)})", resultOutcome); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + + await AssertOutcomeAsync(outcome, ct => + new TaskCompletionSource().Task.WaitAsync(InvalidTimeout, ct), source.Token); + await AssertResultOutcomeAsync(resultOutcome, ct => + new TaskCompletionSource().Task.WaitAsync(InvalidTimeout, ct), source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(10)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithLongTimeoutAndControlledCompletion() + { + // A finite timeout must not be able to win a race against a controlled operation + // that completes the task, no matter which schedule is explored. + this.Test(async () => + { + using var source = new CancellationTokenSource(); + await AssertControlledCompletionAsync(task => task.WaitAsync(LongTimeout)); + await AssertControlledCompletionAsync(task => task.WaitAsync(LongTimeout, source.Token)); + await AssertControlledCompletionAsync(task => task.WaitAsync(LongTimeout, TimeProvider.System)); + await AssertControlledCompletionAsync(task => + task.WaitAsync(LongTimeout, TimeProvider.System, source.Token)); + }, + configuration: this.GetConfiguration().WithTestingIterations(200)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithLongTimeoutAndControlledGenericCompletion() + { + this.Test(async () => + { + using var source = new CancellationTokenSource(); + await AssertControlledResultCompletionAsync(task => task.WaitAsync(LongTimeout)); + await AssertControlledResultCompletionAsync(task => task.WaitAsync(LongTimeout, source.Token)); + await AssertControlledResultCompletionAsync(task => task.WaitAsync(LongTimeout, TimeProvider.System)); + await AssertControlledResultCompletionAsync(task => + task.WaitAsync(LongTimeout, TimeProvider.System, source.Token)); + }, + configuration: this.GetConfiguration().WithTestingIterations(200)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithShortTimeoutAndControlledCompletion() + { + // The size of the timeout must not change the outcome during systematic testing. + this.Test(async () => + { + await AssertControlledCompletionAsync(task => task.WaitAsync(FiniteTimeout)); + await AssertControlledResultCompletionAsync(task => task.WaitAsync(FiniteTimeout)); + }, + configuration: this.GetConfiguration().WithTestingIterations(200)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithFiniteTimeoutAndControlledCancellation() + { + // Cancellation must still be able to terminate a wait with a finite timeout. + this.Test(async () => + { + using var source = new CancellationTokenSource(); + Task canceler = Task.Run(() => source.Cancel()); + await AssertOutcomeAsync(WaitAsyncProvider.WaitTokenCanceledOutcome, ct => + new TaskCompletionSource().Task.WaitAsync(LongTimeout, ct), source.Token); + await canceler; + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithZeroTimeoutAndIncompleteTask() + { + using var uncontrolled = new CancellationTokenSource(); + + // A zero timeout expires before the task gets any chance to complete. + string outcome = WaitAsyncProvider.GetOutcome( + WaitAsyncProvider.CreatePendingTask(), TimeSpan.Zero, uncontrolled.Token); + string timeProviderOutcome = WaitAsyncProvider.GetOutcomeWithTimeProvider( + WaitAsyncProvider.CreatePendingTask(), TimeSpan.Zero, uncontrolled.Token); + string resultOutcome = WaitAsyncProvider.GetResultOutcome( + WaitAsyncProvider.CreatePendingResultTask(), TimeSpan.Zero, uncontrolled.Token); + string resultTimeProviderOutcome = WaitAsyncProvider.GetResultOutcomeWithTimeProvider( + WaitAsyncProvider.CreatePendingResultTask(), TimeSpan.Zero, uncontrolled.Token); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, outcome); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, timeProviderOutcome); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, resultOutcome); + Assert.Equal(WaitAsyncProvider.TimedOutOutcome, resultTimeProviderOutcome); + + this.Test(async () => + { + using var source = new CancellationTokenSource(); + + await AssertOutcomeAsync(outcome, _ => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero), source.Token); + await AssertOutcomeAsync(timeProviderOutcome, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, TimeProvider.System, ct), + source.Token); + await AssertResultOutcomeAsync(resultOutcome, _ => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero), source.Token); + await AssertResultOutcomeAsync(resultTimeProviderOutcome, ct => + new TaskCompletionSource().Task.WaitAsync(TimeSpan.Zero, TimeProvider.System, ct), + source.Token); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithUncompletableTask() + { + // A wait that no controlled operation can complete is reported as a deadlock, + // instead of hanging the test or spuriously timing out. + this.TestWithError(async () => + { + var tcs = new TaskCompletionSource(); + await tcs.Task.WaitAsync(FiniteTimeout); + }, + errorChecker: (e) => + { + Assert.StartsWith("Deadlock detected.", e); + }, + replay: true); + } + + [Fact(Timeout = 5000)] + public void TestWaitAsyncWithUncompletableGenericTaskAndCancellationToken() + { + this.TestWithError(async () => + { + using var source = new CancellationTokenSource(); + var tcs = new TaskCompletionSource(); + await tcs.Task.WaitAsync(LongTimeout, TimeProvider.System, source.Token); + }, + errorChecker: (e) => + { + Assert.StartsWith("Deadlock detected.", e); + }, + replay: true); + } + + /// + /// Asserts that a wait for a task that is completed by another controlled operation + /// completes, instead of spuriously timing out. + /// + private static async Task AssertControlledCompletionAsync(Func wait) + { + var tcs = new TaskCompletionSource(); + Task producer = Task.Run(() => tcs.SetResult(true)); + string actual = await GetOutcomeAsync(_ => wait(tcs.Task), default); + Specification.Assert(actual == WaitAsyncProvider.CompletedOutcome, + "Found outcome '{0}' instead of the expected outcome '{1}'.", + actual, WaitAsyncProvider.CompletedOutcome); + await producer; + } + + /// + /// Asserts that a wait for a generic task that is completed by another controlled + /// operation completes, instead of spuriously timing out. + /// + private static async Task AssertControlledResultCompletionAsync(Func, Task> wait) + { + var tcs = new TaskCompletionSource(); + Task producer = Task.Run(() => tcs.SetResult(WaitAsyncProvider.ExpectedResult)); + string actual = await GetResultOutcomeAsync(_ => wait(tcs.Task), default); + string expected = WaitAsyncProvider.GetCompletedOutcome(WaitAsyncProvider.ExpectedResult); + Specification.Assert(actual == expected, + "Found outcome '{0}' instead of the expected outcome '{1}'.", actual, expected); + await producer; + } + + private static async Task AssertOutcomeAsync(string expected, Func operation, + CancellationToken cancellationToken) + { + string actual = await GetOutcomeAsync(operation, cancellationToken); + Specification.Assert(actual == expected, + "Found outcome '{0}' instead of the uncontrolled outcome '{1}'.", actual, expected); + } + + private static async Task AssertResultOutcomeAsync(string expected, + Func> operation, CancellationToken cancellationToken) + { + string actual = await GetResultOutcomeAsync(operation, cancellationToken); + Specification.Assert(actual == expected, + "Found outcome '{0}' instead of the uncontrolled outcome '{1}'.", actual, expected); + } + + private static async Task GetOutcomeAsync(Func operation, + CancellationToken cancellationToken) + { + try + { + await operation(cancellationToken); + return WaitAsyncProvider.CompletedOutcome; + } + catch (Exception ex) when (!(ex is ThreadInterruptedException)) + { + return WaitAsyncProvider.GetExceptionOutcome(ex, cancellationToken); + } + } + + private static async Task GetResultOutcomeAsync(Func> operation, + CancellationToken cancellationToken) + { + try + { + return WaitAsyncProvider.GetCompletedOutcome(await operation(cancellationToken)); + } + catch (Exception ex) when (!(ex is ThreadInterruptedException)) + { + return WaitAsyncProvider.GetExceptionOutcome(ex, cancellationToken); + } + } + } +} +#endif diff --git a/Tests/Tests.BugFinding/Tests.BugFinding.csproj b/Tests/Tests.BugFinding/Tests.BugFinding.csproj index fb6eb5d59..08785b3dd 100644 --- a/Tests/Tests.BugFinding/Tests.BugFinding.csproj +++ b/Tests/Tests.BugFinding/Tests.BugFinding.csproj @@ -7,7 +7,7 @@ false false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020,xUnit1030,xUnit1031 @@ -19,8 +19,8 @@ - - + + diff --git a/Tests/Tests.Common/Tasks/WaitAsyncProvider.cs b/Tests/Tests.Common/Tasks/WaitAsyncProvider.cs new file mode 100644 index 000000000..9d8f2d6c8 --- /dev/null +++ b/Tests/Tests.Common/Tasks/WaitAsyncProvider.cs @@ -0,0 +1,181 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET +using System; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Coyote.Tests.Common.Tasks +{ + /// + /// Helper class that invokes the uncontrolled task wait overloads and classifies their outcome. + /// + /// + /// We do not rewrite this class in purpose, so that tests can compare the outcome of the + /// controlled overloads against the outcome of the uncontrolled runtime overloads. + /// + public static class WaitAsyncProvider + { + /// + /// The result of a task that completes successfully with a result. + /// + public const int ExpectedResult = 7; + + /// + /// The message of the exception thrown by a faulted task. + /// + public const string ExpectedFaultMessage = "expected fault"; + + /// + /// The outcome of a wait that completed successfully. + /// + public const string CompletedOutcome = "completed"; + + /// + /// The outcome of a wait that timed out. + /// + public const string TimedOutOutcome = "timeout"; + + /// + /// The outcome of a wait that was canceled with the token passed to the wait. + /// + public const string WaitTokenCanceledOutcome = "canceled(waitToken)"; + + /// + /// The outcome of a wait that was canceled with a token other than the one passed to the wait. + /// + public const string SourceTokenCanceledOutcome = "canceled(sourceToken)"; + + /// + /// Creates a task that never completes. + /// + public static Task CreatePendingTask() => new TaskCompletionSource().Task; + + /// + /// Creates a generic task that never completes. + /// + public static Task CreatePendingResultTask() => new TaskCompletionSource().Task; + + /// + /// Creates a task that has already completed successfully. + /// + public static Task CreateCompletedTask() => Task.CompletedTask; + + /// + /// Creates a generic task that has already completed successfully. + /// + public static Task CreateCompletedResultTask() => Task.FromResult(ExpectedResult); + + /// + /// Creates a task that has already faulted. + /// + public static Task CreateFaultedTask() => + Task.FromException(new InvalidOperationException(ExpectedFaultMessage)); + + /// + /// Creates a generic task that has already faulted. + /// + public static Task CreateFaultedResultTask() => + Task.FromException(new InvalidOperationException(ExpectedFaultMessage)); + + /// + /// Creates a task that has already been canceled with the specified token. + /// + public static Task CreateCanceledTask(CancellationToken cancellationToken) => + Task.FromCanceled(cancellationToken); + + /// + /// Creates a generic task that has already been canceled with the specified token. + /// + public static Task CreateCanceledResultTask(CancellationToken cancellationToken) => + Task.FromCanceled(cancellationToken); + + /// + /// Returns the outcome of waiting for the specified task with the specified cancellation token. + /// + public static string GetOutcome(Task task, CancellationToken cancellationToken) => + Classify(() => task.WaitAsync(cancellationToken), cancellationToken); + + /// + /// Returns the outcome of waiting for the specified task with the specified timeout and token. + /// + public static string GetOutcome(Task task, TimeSpan timeout, CancellationToken cancellationToken) => + Classify(() => task.WaitAsync(timeout, cancellationToken), cancellationToken); + + /// + /// Returns the outcome of waiting for the specified generic task with the specified token. + /// + public static string GetResultOutcome(Task task, CancellationToken cancellationToken) => + ClassifyResult(() => task.WaitAsync(cancellationToken), cancellationToken); + + /// + /// Returns the outcome of waiting for the specified generic task with the specified timeout and token. + /// + public static string GetResultOutcome(Task task, TimeSpan timeout, + CancellationToken cancellationToken) => + ClassifyResult(() => task.WaitAsync(timeout, cancellationToken), cancellationToken); + +#if NET8_0_OR_GREATER + /// + /// Returns the outcome of waiting for the specified task with the specified timeout, time + /// provider and token. + /// + public static string GetOutcomeWithTimeProvider(Task task, TimeSpan timeout, + CancellationToken cancellationToken) => + Classify(() => task.WaitAsync(timeout, TimeProvider.System, cancellationToken), cancellationToken); + + /// + /// Returns the outcome of waiting for the specified generic task with the specified timeout, + /// time provider and token. + /// + public static string GetResultOutcomeWithTimeProvider(Task task, TimeSpan timeout, + CancellationToken cancellationToken) => + ClassifyResult(() => task.WaitAsync(timeout, TimeProvider.System, cancellationToken), cancellationToken); +#endif + + /// + /// Returns the outcome of a task that completed successfully with the specified result. + /// + public static string GetCompletedOutcome(TResult result) => $"{CompletedOutcome}(result={result})"; + + /// + /// Returns the outcome that corresponds to the specified exception. + /// + public static string GetExceptionOutcome(Exception exception, CancellationToken cancellationToken) => + exception switch + { + OperationCanceledException ex => ex.CancellationToken == cancellationToken ? + WaitTokenCanceledOutcome : SourceTokenCanceledOutcome, + TimeoutException => TimedOutOutcome, + _ => $"fault({exception.GetType().Name})" + }; + + private static string Classify(Func operation, CancellationToken cancellationToken) + { + try + { + operation().GetAwaiter().GetResult(); + return CompletedOutcome; + } + catch (Exception ex) + { + return GetExceptionOutcome(ex, cancellationToken); + } + } + + private static string ClassifyResult(Func> operation, + CancellationToken cancellationToken) + { + try + { + return GetCompletedOutcome(operation().GetAwaiter().GetResult()); + } + catch (Exception ex) + { + return GetExceptionOutcome(ex, cancellationToken); + } + } + } +} +#endif diff --git a/Tests/Tests.Common/Tests.Common.csproj b/Tests/Tests.Common/Tests.Common.csproj index b33d5095e..29534ef8e 100644 --- a/Tests/Tests.Common/Tests.Common.csproj +++ b/Tests/Tests.Common/Tests.Common.csproj @@ -6,7 +6,7 @@ .\bin\ false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020 @@ -14,6 +14,6 @@ - + \ No newline at end of file diff --git a/Tests/Tests.Rewriting/Methods/AsyncMethodRewritingTests.cs b/Tests/Tests.Rewriting/Methods/AsyncMethodRewritingTests.cs index fe118f7d1..c14cbc7c4 100644 --- a/Tests/Tests.Rewriting/Methods/AsyncMethodRewritingTests.cs +++ b/Tests/Tests.Rewriting/Methods/AsyncMethodRewritingTests.cs @@ -25,5 +25,17 @@ public async Task TestRewritingGenericAsyncMethod() { return await Task.FromResult(1); } + + [Fact(Timeout = 5000)] + public async ValueTask TestRewritingAsyncValueTaskMethod() + { + await Task.CompletedTask; + } + + [Fact(Timeout = 5000)] + public async ValueTask TestRewritingGenericAsyncValueTaskMethod() + { + return await Task.FromResult(1); + } } } diff --git a/Tests/Tests.Rewriting/Methods/HostRuntimeValidationTests.cs b/Tests/Tests.Rewriting/Methods/HostRuntimeValidationTests.cs new file mode 100644 index 000000000..b9d54f74d --- /dev/null +++ b/Tests/Tests.Rewriting/Methods/HostRuntimeValidationTests.cs @@ -0,0 +1,373 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET +using System; +using System.IO; +using System.Linq; +using System.Runtime.Versioning; +using System.Security.Cryptography; +using Microsoft.Coyote.Logging; +using Microsoft.Coyote.Runtime; +using Mono.Cecil; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.Rewriting.Tests +{ + public class HostRuntimeValidationTests : BaseRewritingTest + { + /// + /// The assembly used as the source of every synthesized rewriting target. It is small and + /// it targets the same framework as the running host. + /// + private const string RewritingSourceAssembly = "Microsoft.Coyote.Tests.Rewriting.Helpers.dll"; + + public HostRuntimeValidationTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestMatchingTargetFrameworkMetadataIsAccepted() + { + string assemblyPath = typeof(HostRuntimeValidationTests).Assembly.Location; + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath); + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath); + } + + [Fact(Timeout = 5000)] + public void TestMissingTargetFrameworkMetadataIsAccepted() + { + string assemblyPath = CreateAssemblyWithTargetFramework(null); + try + { + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath); + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Fact(Timeout = 5000)] + public void TestMalformedTargetFrameworkMetadataIsAccepted() + { + string assemblyPath = CreateAssemblyWithTargetFramework("not-a-framework"); + try + { + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath); + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Fact(Timeout = 5000)] + public void TestNonCoreTargetFrameworkMetadataIsAccepted() + { + string assemblyPath = CreateAssemblyWithTargetFramework(".NETStandard,Version=v2.0"); + try + { + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath); + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Fact(Timeout = 5000)] + public void TestNewerTargetFrameworkHasAnActionableDiagnostic() + { + int targetMajorVersion = Environment.Version.Major + 1; + string targetFramework = $".NETCoreApp,Version=v{targetMajorVersion}.0"; + string assemblyPath = CreateAssemblyWithTargetFramework(targetFramework); + try + { + var exception = Assert.Throws(() => + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath)); + + Assert.Contains($"The Coyote host is running on .NET {Environment.Version.Major}.{Environment.Version.Minor}", + exception.Message); + Assert.Contains($"requires {targetFramework}", exception.Message); + Assert.Contains($"Run the net{targetMajorVersion}.0 Coyote host", exception.Message); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Theory(Timeout = 5000)] + [InlineData(1)] + [InlineData(2)] + public void TestOlderTargetFrameworkIsAcceptedWhenTesting(int majorVersionOffset) + { + // The .NET runtime rolls forward, so a newer host can load an older target assembly. For + // example, the net10.0 host must still be able to test a net8.0 assembly. + int targetMajorVersion = Environment.Version.Major - majorVersionOffset; + string assemblyPath = CreateAssemblyWithTargetFramework($".NETCoreApp,Version=v{targetMajorVersion}.0"); + try + { + TargetRuntimeValidator.ValidateTestingTarget(assemblyPath); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Theory(Timeout = 5000)] + [InlineData(1)] + [InlineData(2)] + public void TestNewerTargetFrameworkIsRejectedWhenRewriting(int majorVersionOffset) + { + // Covers the net8.0 host rejecting a net10.0 target assembly. + int targetMajorVersion = Environment.Version.Major + majorVersionOffset; + string targetFramework = $".NETCoreApp,Version=v{targetMajorVersion}.0"; + string assemblyPath = CreateAssemblyWithTargetFramework(targetFramework); + try + { + var exception = Assert.Throws(() => + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath)); + + Assert.Contains($"The Coyote host is running on .NET {Environment.Version.Major}.{Environment.Version.Minor}", + exception.Message); + Assert.Contains($"targets {targetFramework}", exception.Message); + Assert.Contains($"Run the net{targetMajorVersion}.0 Coyote host to rewrite this assembly", + exception.Message); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Theory(Timeout = 5000)] + [InlineData(1)] + [InlineData(2)] + public void TestOlderTargetFrameworkIsRejectedWhenRewriting(int majorVersionOffset) + { + // Covers the net10.0 host rejecting net9.0 and net8.0 target assemblies. + int targetMajorVersion = Environment.Version.Major - majorVersionOffset; + string targetFramework = $".NETCoreApp,Version=v{targetMajorVersion}.0"; + string assemblyPath = CreateAssemblyWithTargetFramework(targetFramework); + try + { + var exception = Assert.Throws(() => + TargetRuntimeValidator.ValidateRewritingTarget(assemblyPath)); + + Assert.Contains($"The Coyote host is running on .NET {Environment.Version.Major}.{Environment.Version.Minor}", + exception.Message); + Assert.Contains($"targets {targetFramework}", exception.Message); + Assert.Contains( + $"would inject .NET {Environment.Version.Major}.{Environment.Version.Minor} runtime references", + exception.Message); + Assert.Contains($"Run the net{targetMajorVersion}.0 Coyote host to rewrite this assembly", + exception.Message); + } + finally + { + File.Delete(assemblyPath); + } + } + + [Theory(Timeout = 10000)] + [InlineData(1)] + [InlineData(2)] + public void TestRewritingOlderTargetFrameworkDoesNotModifyAssembly(int majorVersionOffset) + { + // Covers the net10.0 host refusing to rewrite net9.0 and net8.0 target assemblies. Before + // this validation existed, rewriting reported success but injected .NET 10 references that + // made the target unloadable on its own runtime. + int targetMajorVersion = Environment.Version.Major - majorVersionOffset; + this.AssertRewritingIsRejectedWithoutModifyingAssembly($".NETCoreApp,Version=v{targetMajorVersion}.0"); + } + + [Theory(Timeout = 10000)] + [InlineData(1)] + [InlineData(2)] + public void TestRewritingNewerTargetFrameworkDoesNotModifyAssembly(int majorVersionOffset) + { + // Covers the net8.0 host refusing to rewrite a net10.0 target assembly. + int targetMajorVersion = Environment.Version.Major + majorVersionOffset; + this.AssertRewritingIsRejectedWithoutModifyingAssembly($".NETCoreApp,Version=v{targetMajorVersion}.0"); + } + + [Fact(Timeout = 10000)] + public void TestRewritingSameTargetFrameworkSucceeds() + { + string directory = CreateScratchDirectory(); + try + { + string assemblyPath = CreateRewritingTarget(directory, + $".NETCoreApp,Version=v{Environment.Version.Major}.0"); + RunRewritingEngine(directory, assemblyPath); + + using AssemblyDefinition definition = ReadAssembly(assemblyPath); + Assert.Contains(definition.CustomAttributes, attribute => + attribute.AttributeType.FullName == typeof(RewritingSignatureAttribute).FullName); + + foreach (AssemblyNameReference reference in definition.MainModule.AssemblyReferences.Where( + candidate => candidate.Name is "System.Runtime" || candidate.Name is "System.Private.CoreLib")) + { + Assert.Equal(Environment.Version.Major, reference.Version.Major); + } + } + finally + { + Directory.Delete(directory, true); + } + } + + /// + /// Asserts that rewriting an assembly declaring the specified target framework is rejected + /// before the assembly, or any other output, is written. + /// + private void AssertRewritingIsRejectedWithoutModifyingAssembly(string targetFramework) + { + string directory = CreateScratchDirectory(); + try + { + string assemblyPath = CreateRewritingTarget(directory, targetFramework); + byte[] hash = ComputeHash(assemblyPath); + + var exception = Assert.Throws(() => + RunRewritingEngine(directory, assemblyPath)); + this.TestOutput.WriteLine(exception.Message); + + Assert.Contains($"targets {targetFramework}", exception.Message); + Assert.Contains("Coyote host to rewrite this assembly", exception.Message); + + // The target assembly must be left untouched and no output must have been produced. + Assert.Equal(hash, ComputeHash(assemblyPath)); + Assert.Equal(new[] { assemblyPath }, Directory.GetFiles(directory, "*", SearchOption.AllDirectories)); + Assert.Empty(Directory.GetDirectories(directory)); + + using AssemblyDefinition definition = ReadAssembly(assemblyPath); + Assert.DoesNotContain(definition.CustomAttributes, attribute => + attribute.AttributeType.FullName == typeof(RewritingSignatureAttribute).FullName); + } + finally + { + Directory.Delete(directory, true); + } + } + + /// + /// Runs the rewriting engine over the specified assembly, replacing it in place. + /// + private static void RunRewritingEngine(string directory, string assemblyPath) + { + var options = RewritingOptions.Create(); + options.AssembliesDirectory = directory; + options.OutputDirectory = directory; + options.AssemblyPaths.Add(assemblyPath); + + var configuration = Microsoft.Coyote.Configuration.Create(); + using var logWriter = new LogWriter(configuration); + RewritingEngine.Run(options, configuration, logWriter, new Profiler()); + } + + /// + /// Creates a new empty directory that is local to the test binaries. + /// + private static string CreateScratchDirectory() => Directory.CreateDirectory(Path.Combine( + Path.GetDirectoryName(typeof(HostRuntimeValidationTests).Assembly.Location), + nameof(HostRuntimeValidationTests), + Guid.NewGuid().ToString("N"))).FullName; + + /// + /// Copies an assembly that can be rewritten to the specified directory, declaring the + /// specified target framework and dropping any existing rewriting signature. + /// + private static string CreateRewritingTarget(string directory, string targetFramework) + { + string sourcePath = Path.Combine( + Path.GetDirectoryName(typeof(HostRuntimeValidationTests).Assembly.Location), + RewritingSourceAssembly); + Assert.True(File.Exists(sourcePath), $"File not found: {sourcePath}"); + + string outputPath = Path.Combine(directory, RewritingSourceAssembly); + using (AssemblyDefinition definition = ReadAssembly(sourcePath)) + { + RemoveCustomAttributes(definition, typeof(RewritingSignatureAttribute).FullName); + SetTargetFramework(definition, targetFramework); + definition.Write(outputPath); + } + + return outputPath; + } + + /// + /// Creates a copy of the test assembly declaring the specified target framework. + /// + private static string CreateAssemblyWithTargetFramework(string targetFramework) + { + string sourcePath = typeof(HostRuntimeValidationTests).Assembly.Location; + string outputPath = Path.Combine( + Path.GetDirectoryName(sourcePath), + $"{nameof(HostRuntimeValidationTests)}.{Guid.NewGuid():N}.dll"); + + using (AssemblyDefinition definition = ReadAssembly(sourcePath)) + { + SetTargetFramework(definition, targetFramework); + definition.Write(outputPath); + } + + return outputPath; + } + + /// + /// Reads the specified assembly without keeping the file on disk locked. + /// + private static AssemblyDefinition ReadAssembly(string assemblyPath) => + AssemblyDefinition.ReadAssembly(assemblyPath, new ReaderParameters { InMemory = true }); + + /// + /// Replaces the target framework metadata of the specified assembly, or removes + /// it if no target framework is specified. + /// + private static void SetTargetFramework(AssemblyDefinition definition, string targetFramework) + { + RemoveCustomAttributes(definition, typeof(TargetFrameworkAttribute).FullName); + if (targetFramework != null) + { + var constructor = definition.MainModule.ImportReference( + typeof(TargetFrameworkAttribute).GetConstructor(new[] { typeof(string) })); + var replacement = new CustomAttribute(constructor); + replacement.ConstructorArguments.Add(new CustomAttributeArgument( + definition.MainModule.TypeSystem.String, targetFramework)); + definition.CustomAttributes.Add(replacement); + } + } + + /// + /// Removes all assembly-level custom attributes with the specified type name. + /// + private static void RemoveCustomAttributes(AssemblyDefinition definition, string attributeTypeName) + { + foreach (CustomAttribute attribute in definition.CustomAttributes.Where( + candidate => candidate.AttributeType.FullName == attributeTypeName).ToArray()) + { + definition.CustomAttributes.Remove(attribute); + } + } + + /// + /// Computes the hash of the specified file. + /// + private static byte[] ComputeHash(string path) + { + using var stream = File.OpenRead(path); + using var algorithm = SHA256.Create(); + return algorithm.ComputeHash(stream); + } + } +} +#endif diff --git a/Tests/Tests.Rewriting/Methods/UnsupportedSynchronizationRewritingTests.cs b/Tests/Tests.Rewriting/Methods/UnsupportedSynchronizationRewritingTests.cs new file mode 100644 index 000000000..33a9b26fe --- /dev/null +++ b/Tests/Tests.Rewriting/Methods/UnsupportedSynchronizationRewritingTests.cs @@ -0,0 +1,50 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System.Threading; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.Rewriting.Tests +{ + public class UnsupportedSynchronizationRewritingTests : BaseRewritingTest + { + public UnsupportedSynchronizationRewritingTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestBarrierIsReportedAsUncontrolledSynchronization() + { + this.TestWithError(() => + { + using var barrier = new Barrier(1); + barrier.SignalAndWait(); + }, + errorChecker: (e) => + { + Assert.StartsWith( + $"Invoking '{typeof(Barrier).FullName}..ctor' is not intercepted", + e); + }); + } + + [Fact(Timeout = 5000)] + public void TestCountdownEventIsReportedAsUncontrolledSynchronization() + { + this.TestWithError(() => + { + using var countdown = new CountdownEvent(1); + countdown.Signal(); + countdown.Wait(); + }, + errorChecker: (e) => + { + Assert.StartsWith( + $"Invoking '{typeof(CountdownEvent).FullName}..ctor' is not intercepted", + e); + }); + } + } +} diff --git a/Tests/Tests.Rewriting/Tests.Rewriting.csproj b/Tests/Tests.Rewriting/Tests.Rewriting.csproj index c4e452dfe..a34222510 100644 --- a/Tests/Tests.Rewriting/Tests.Rewriting.csproj +++ b/Tests/Tests.Rewriting/Tests.Rewriting.csproj @@ -6,15 +6,15 @@ .\bin\ false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit1028,xUnit2020,xUnit1030,xUnit1031 - - + + diff --git a/Tests/Tests.Rewriting/Types/LockRewritingTests.cs b/Tests/Tests.Rewriting/Types/LockRewritingTests.cs new file mode 100644 index 000000000..4b07fad7f --- /dev/null +++ b/Tests/Tests.Rewriting/Types/LockRewritingTests.cs @@ -0,0 +1,301 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET10_0_OR_GREATER +using System; +using System.Collections.Generic; +using System.IO; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.Coyote.Runtime; +using Microsoft.Coyote.Specifications; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.Rewriting.Tests +{ + public class LockRewritingTests : BaseRewritingTest + { + public LockRewritingTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockMutualExclusion() + { + this.Test(() => + { + var gate = new Lock(); + int entered = 0; + Task first = Task.Run(() => Enter(gate, ref entered)); + Task second = Task.Run(() => Enter(gate, ref entered)); + Task.WaitAll(first, second); + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockLoweringUsesControlledEnterScope() + { + string assemblyPath = typeof(LockRewritingTests).Assembly.Location; + string diff = File.ReadAllText(Path.ChangeExtension(assemblyPath, ".diff.json")); + Assert.Contains( + "System.Threading.Lock/Scope System.Threading.Lock::EnterScope()", + diff); + Assert.Contains( + "Microsoft.Coyote.Rewriting.Types.Threading.Lock::EnterScope(System.Threading.Lock)", + diff); + } + + [Fact(Timeout = 5000)] + public void TestRewritingNestedLockStatement() + { + this.Test(() => + { + var gate = new Lock(); + lock (gate) + { + Assert.True(gate.IsHeldByCurrentThread); + lock (gate) + { + Assert.True(gate.IsHeldByCurrentThread); + } + + Assert.True(gate.IsHeldByCurrentThread); + } + + Assert.False(gate.IsHeldByCurrentThread); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockScopeReleaseOnException() + { + this.Test(() => + { + var gate = new Lock(); + Action throwInsideLock = () => + { + lock (gate) + { + throw new InvalidOperationException(); + } + }; + Assert.Throws(throwInsideLock); + + Assert.False(gate.IsHeldByCurrentThread); + gate.Enter(); + gate.Exit(); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingDefaultAndCopiedLockScope() + { + this.Test(() => + { + var gate = new Lock(); + Lock.Scope emptyScope = default; + emptyScope.Dispose(); + + Lock.Scope scope = gate.EnterScope(); + Lock.Scope copiedScope = scope; + Assert.True(gate.IsHeldByCurrentThread); + scope.Dispose(); + Assert.False(gate.IsHeldByCurrentThread); + try + { + copiedScope.Dispose(); + Assert.True(false, "Disposing a copied scope should fail after the original scope exits."); + } + catch (SynchronizationLockException) + { + } + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockTryEnterVariants() + { + this.Test(() => + { + var gate = new Lock(); + Assert.True(gate.TryEnter()); + Assert.True(gate.TryEnter(0)); + Assert.True(gate.TryEnter(Timeout.Infinite)); + Assert.True(gate.TryEnter(TimeSpan.Zero)); + Assert.True(gate.TryEnter(Timeout.InfiniteTimeSpan)); + Assert.True(gate.IsHeldByCurrentThread); + gate.Exit(); + gate.Exit(); + gate.Exit(); + gate.Exit(); + gate.Exit(); + + Assert.Throws(() => gate.TryEnter(-2)); + Assert.Throws(() => gate.TryEnter(TimeSpan.FromMilliseconds(-2))); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockFiniteTimeoutIsExplicitlyUnsupported() + { + this.TestWithError(() => + { + var gate = new Lock(); + Task owner = Task.Run(() => + { + gate.Enter(); + SchedulingPoint.Interleave(); + gate.Exit(); + }); + + Task contender = Task.Run(() => + { + SchedulingPoint.Interleave(); + if (gate.TryEnter(1)) + { + gate.Exit(); + } + }); + + Task.WaitAll(owner, contender); + }, + configuration: this.GetConfiguration().WithTestingIterations(100), + expectedError: "Invoking 'Lock.TryEnter' with a finite timeout is not supported in systematic testing."); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockTryEnterWithLockAccessRaceChecking() + { + this.Test(() => + { + var gate = new Lock(); + int entered = 0; + Task first = Task.Run(() => TryEnter(gate, ref entered)); + Task second = Task.Run(() => TryEnter(gate, ref entered)); + Task.WaitAll(first, second); + }, + configuration: this.GetConfiguration().WithLockAccessRaceCheckingEnabled().WithTestingIterations(100)); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockContentionExploresBothAcquisitionOrders() + { + var winners = new HashSet(); + this.Test(() => + { + var gate = new Lock(); + int winner = 0; + Task first = Task.Run(() => + { + lock (gate) + { + if (winner is 0) + { + winner = 1; + } + + SchedulingPoint.Interleave(); + } + }); + + Task second = Task.Run(() => + { + lock (gate) + { + if (winner is 0) + { + winner = 2; + } + + SchedulingPoint.Interleave(); + } + }); + + Task.WaitAll(first, second); + lock (winners) + { + winners.Add(winner); + } + }, + configuration: this.GetConfiguration().WithTestingIterations(100)); + + Assert.Contains(1, winners); + Assert.Contains(2, winners); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockDeadlockDetection() + { + this.TestWithError(() => + { + var firstGate = new Lock(); + var secondGate = new Lock(); + Task first = Task.Run(() => + { + lock (firstGate) + { + SchedulingPoint.Interleave(); + lock (secondGate) + { + } + } + }); + + Task second = Task.Run(() => + { + lock (secondGate) + { + SchedulingPoint.Interleave(); + lock (firstGate) + { + } + } + }); + + Task.WaitAll(first, second); + }, + configuration: this.GetConfiguration().WithTestingIterations(100), + errorChecker: (e) => Assert.StartsWith("Deadlock detected.", e)); + } + + [Fact(Timeout = 5000)] + public void TestRewritingLockNonOwnerExit() + { + this.TestWithException(async () => + { + var gate = new Lock(); + gate.Enter(); + await Task.Run(() => gate.Exit()); + }); + } + + private static void Enter(Lock gate, ref int entered) + { + lock (gate) + { + entered++; + Specification.Assert(entered is 1, "More than one operation entered the lock."); + SchedulingPoint.Interleave(); + entered--; + } + } + + private static void TryEnter(Lock gate, ref int entered) + { + while (!gate.TryEnter()) + { + SchedulingPoint.Interleave(); + } + + entered++; + Specification.Assert(entered is 1, "More than one operation entered the lock."); + SchedulingPoint.Interleave(); + entered--; + gate.Exit(); + } + } +} +#endif diff --git a/Tests/Tests.Rewriting/Types/RuntimeApiDiffGateTests.cs b/Tests/Tests.Rewriting/Types/RuntimeApiDiffGateTests.cs new file mode 100644 index 000000000..e54d9826e --- /dev/null +++ b/Tests/Tests.Rewriting/Types/RuntimeApiDiffGateTests.cs @@ -0,0 +1,394 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Reflection; +using System.Threading; +using System.Threading.Tasks; +using Xunit; +using Xunit.Abstractions; + +using CoyoteInterlocked = Microsoft.Coyote.Rewriting.Types.Threading.Interlocked; +using CoyoteMonitor = Microsoft.Coyote.Rewriting.Types.Threading.Monitor; +using CoyoteSemaphoreSlim = Microsoft.Coyote.Rewriting.Types.Threading.SemaphoreSlim; +using CoyoteTask = Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task; +using CoyoteThread = Microsoft.Coyote.Rewriting.Types.Threading.Thread; +using CoyoteWaitHandle = Microsoft.Coyote.Rewriting.Types.Threading.WaitHandle; +#if NET10_0_OR_GREATER +using CoyoteLock = Microsoft.Coyote.Rewriting.Types.Threading.Lock; +#endif + +namespace Microsoft.Coyote.Rewriting.Tests +{ + public class RuntimeApiDiffGateTests : BaseRewritingTest + { + public RuntimeApiDiffGateTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestCurrentRuntimeSignaturesAreExactlyClassified() + { + IReadOnlyList runtimeMembers = GetRuntimeMembers(); + IReadOnlyCollection runtimeSignatures = runtimeMembers.Select(member => member.Signature).ToArray(); + IReadOnlyCollection supportedSignatures = runtimeMembers + .Where(member => member.IsSupported) + .Select(member => member.Signature) + .ToArray(); + IReadOnlyCollection replacementSignatures = runtimeMembers + .Where(member => member.IsSupported && HasReplacement(member)) + .Select(member => member.Signature) + .ToArray(); + + IReadOnlyList errors = ApiDiffGate.Classify( + runtimeSignatures, + supportedSignatures, + replacementSignatures, + GetUnsupportedSignatures(runtimeMembers)); + Assert.True(errors.Count is 0, string.Join(Environment.NewLine, errors)); + } + + [Fact(Timeout = 5000)] + public void TestAddedRuntimeMethodFailsTheGate() + { + IReadOnlyList runtimeMembers = GetRuntimeMembers(); + IReadOnlyCollection runtimeSignatures = runtimeMembers.Select(member => member.Signature) + .Concat(new[] { "System.Threading.Tasks.Task|instance|AddedByANewRuntime()|System.Void" }) + .ToArray(); + IReadOnlyCollection supportedSignatures = runtimeMembers + .Where(member => member.IsSupported) + .Select(member => member.Signature) + .ToArray(); + IReadOnlyCollection replacementSignatures = runtimeMembers + .Where(member => member.IsSupported && HasReplacement(member)) + .Select(member => member.Signature) + .ToArray(); + + string error = Assert.Single(ApiDiffGate.Classify( + runtimeSignatures, + supportedSignatures, + replacementSignatures, + GetUnsupportedSignatures(runtimeMembers))); + Assert.Contains("Unclassified runtime signature", error); + Assert.Contains("AddedByANewRuntime", error); + } + + [Fact(Timeout = 5000)] + public void TestMissingSupportedReplacementMethodFailsTheGate() + { + IReadOnlyList runtimeMembers = GetRuntimeMembers(); + ApiMember requiredMember = runtimeMembers.First(member => member.IsSupported); + IReadOnlyCollection runtimeSignatures = runtimeMembers.Select(member => member.Signature).ToArray(); + IReadOnlyCollection supportedSignatures = runtimeMembers + .Where(member => member.IsSupported) + .Select(member => member.Signature) + .ToArray(); + IReadOnlyCollection replacementSignatures = runtimeMembers + .Where(member => member.IsSupported && member.Signature != requiredMember.Signature && HasReplacement(member)) + .Select(member => member.Signature) + .ToArray(); + + string error = Assert.Single(ApiDiffGate.Classify( + runtimeSignatures, + supportedSignatures, + replacementSignatures, + GetUnsupportedSignatures(runtimeMembers))); + Assert.Contains("Missing controlled replacement", error); + Assert.Contains(requiredMember.Signature, error); + } + + [Fact(Timeout = 5000)] + public void TestAllowlistedMethodsRequireANonemptyReason() + { + IReadOnlyList runtimeMembers = GetRuntimeMembers(); + ApiMember unsupportedMember = runtimeMembers.Single(member => !member.IsSupported); + IReadOnlyCollection runtimeSignatures = runtimeMembers.Select(member => member.Signature).ToArray(); + IReadOnlyCollection supportedSignatures = runtimeMembers + .Where(member => member.IsSupported) + .Select(member => member.Signature) + .ToArray(); + IReadOnlyCollection replacementSignatures = runtimeMembers + .Where(member => member.IsSupported && HasReplacement(member)) + .Select(member => member.Signature) + .ToArray(); + var unsupported = new Dictionary(GetUnsupportedSignatures(runtimeMembers)) + { + [unsupportedMember.Signature] = string.Empty + }; + + string error = Assert.Single(ApiDiffGate.Classify( + runtimeSignatures, + supportedSignatures, + replacementSignatures, + unsupported)); + Assert.Contains("nonempty reason", error); + Assert.Contains(unsupportedMember.Signature, error); + } + + private static IReadOnlyList GetRuntimeMembers() + { + var members = new List + { +#if NET6_0_OR_GREATER + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAsync), typeof(CancellationToken)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAsync), typeof(TimeSpan)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAsync), typeof(TimeSpan), typeof(CancellationToken)), +#endif +#if NET8_0_OR_GREATER + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAsync), typeof(TimeSpan), typeof(TimeProvider)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAsync), typeof(TimeSpan), typeof(TimeProvider), + typeof(CancellationToken)), +#endif +#if NET6_0_OR_GREATER + Create(typeof(Task<>), typeof(Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task<>), + nameof(Task.WaitAsync), typeof(CancellationToken)), + Create(typeof(Task<>), typeof(Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task<>), + nameof(Task.WaitAsync), typeof(TimeSpan)), + Create(typeof(Task<>), typeof(Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task<>), + nameof(Task.WaitAsync), typeof(TimeSpan), typeof(CancellationToken)), +#endif +#if NET8_0_OR_GREATER + Create(typeof(Task<>), typeof(Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task<>), + nameof(Task.WaitAsync), typeof(TimeSpan), typeof(TimeProvider)), + Create(typeof(Task<>), typeof(Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task<>), + nameof(Task.WaitAsync), typeof(TimeSpan), typeof(TimeProvider), typeof(CancellationToken)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.Delay), typeof(TimeSpan), typeof(TimeProvider)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.Delay), typeof(TimeSpan), typeof(TimeProvider), + typeof(CancellationToken)), +#endif + Create(typeof(Monitor), typeof(CoyoteMonitor), nameof(Monitor.Enter), typeof(object)), + Create(typeof(Monitor), typeof(CoyoteMonitor), nameof(Monitor.Exit), typeof(object)), + Create(typeof(Monitor), typeof(CoyoteMonitor), nameof(Monitor.TryEnter), typeof(object)), + Create(typeof(Monitor), typeof(CoyoteMonitor), nameof(Monitor.Wait), typeof(object)), + Create(typeof(SemaphoreSlim), typeof(CoyoteSemaphoreSlim), nameof(SemaphoreSlim.Wait)), + Create(typeof(SemaphoreSlim), typeof(CoyoteSemaphoreSlim), nameof(SemaphoreSlim.WaitAsync)), + Create(typeof(SemaphoreSlim), typeof(CoyoteSemaphoreSlim), nameof(SemaphoreSlim.Release)), + Create(typeof(Interlocked), typeof(CoyoteInterlocked), nameof(Interlocked.Increment), + typeof(int).MakeByRefType()), + Create(typeof(WaitHandle), typeof(CoyoteWaitHandle), nameof(WaitHandle.WaitOne)), + Create(typeof(Thread), typeof(CoyoteThread), nameof(Thread.Sleep), typeof(int)), + Create(typeof(Task), typeof(CoyoteTask), nameof(Task.RunSynchronously), false) + }; + +#if NET10_0_OR_GREATER + members.Add(Create(typeof(Task), typeof(CoyoteTask), nameof(Task.WaitAll), + typeof(IEnumerable), typeof(CancellationToken))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.Enter))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.EnterScope))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.TryEnter))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.TryEnter), typeof(int))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.TryEnter), typeof(TimeSpan))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), nameof(Lock.Exit))); + members.Add(Create(typeof(Lock), typeof(CoyoteLock), "get_IsHeldByCurrentThread")); +#endif + return members; + } + + private static ApiMember Create(Type runtimeType, Type replacementType, string methodName, params Type[] parameterTypes) => + Create(runtimeType, replacementType, methodName, true, parameterTypes); + + private static ApiMember Create(Type runtimeType, Type replacementType, string methodName, bool isSupported, + params Type[] parameterTypes) + { + MethodInfo method = runtimeType.GetMethods( + BindingFlags.Public | BindingFlags.Instance | BindingFlags.Static | BindingFlags.DeclaredOnly) + .Single(candidate => candidate.Name == methodName && ParametersMatch(candidate, parameterTypes)); + return new ApiMember(method, replacementType, isSupported); + } + + private static bool ParametersMatch(MethodInfo method, IReadOnlyList parameterTypes) + { + ParameterInfo[] parameters = method.GetParameters(); + if (parameters.Length != parameterTypes.Count) + { + return false; + } + + for (int idx = 0; idx < parameters.Length; idx++) + { + if (parameters[idx].ParameterType != parameterTypes[idx]) + { + return false; + } + } + + return true; + } + + private static bool HasReplacement(ApiMember member) + { + MethodInfo runtimeMethod = member.RuntimeMethod; + foreach (MethodInfo replacementMethod in member.ReplacementType.GetMethods( + BindingFlags.Public | BindingFlags.Static | BindingFlags.DeclaredOnly)) + { + if (replacementMethod.Name != runtimeMethod.Name) + { + continue; + } + + ParameterInfo[] replacementParameters = replacementMethod.GetParameters(); + ParameterInfo[] runtimeParameters = runtimeMethod.GetParameters(); + int offset = runtimeMethod.IsStatic ? 0 : 1; + if (replacementParameters.Length != runtimeParameters.Length + offset || + !TypeShapesMatch(replacementMethod.ReturnType, runtimeMethod.ReturnType)) + { + continue; + } + + if (!runtimeMethod.IsStatic && + !TypeShapesMatch(replacementParameters[0].ParameterType, runtimeMethod.DeclaringType)) + { + continue; + } + + bool matched = true; + for (int idx = 0; idx < runtimeParameters.Length; idx++) + { + if (!TypeShapesMatch(replacementParameters[idx + offset].ParameterType, + runtimeParameters[idx].ParameterType)) + { + matched = false; + break; + } + } + + if (matched) + { + return true; + } + } + + return false; + } + + private static bool TypeShapesMatch(Type left, Type right) + { +#if NET10_0_OR_GREATER + if (left == typeof(CoyoteLock.Scope) && right == typeof(Lock.Scope)) + { + return true; + } +#endif + return GetTypeShape(left) == GetTypeShape(right); + } + + private static string GetTypeShape(Type type) + { + if (type.IsByRef) + { + return GetTypeShape(type.GetElementType()) + "&"; + } + + if (type.IsArray) + { + return GetTypeShape(type.GetElementType()) + "[]"; + } + + if (type.IsGenericParameter) + { + return "*"; + } + + if (type.IsGenericType) + { + return type.GetGenericTypeDefinition().FullName + "<" + + string.Join(",", type.GetGenericArguments().Select(GetTypeShape)) + ">"; + } + + return type.FullName; + } + + private static string GetMethodSignature(MethodInfo method) + { + string instanceKind = method.IsStatic ? "static" : "instance"; + string parameters = string.Join(",", method.GetParameters().Select(parameter => GetTypeShape(parameter.ParameterType))); + return $"{GetTypeShape(method.DeclaringType)}|{instanceKind}|{method.Name}({parameters})|{GetTypeShape(method.ReturnType)}"; + } + +#if NETFRAMEWORK + private static Dictionary GetUnsupportedSignatures(IEnumerable members) => +#else + private static IReadOnlyDictionary GetUnsupportedSignatures(IEnumerable members) => +#endif + members.Where(member => !member.IsSupported).ToDictionary( + member => member.Signature, + member => "Task.RunSynchronously is intentionally not controlled because it can execute work on an arbitrary scheduler."); + + private sealed class ApiMember + { + internal ApiMember(MethodInfo runtimeMethod, Type replacementType, bool isSupported) + { + this.RuntimeMethod = runtimeMethod; + this.ReplacementType = replacementType; + this.IsSupported = isSupported; + this.Signature = GetMethodSignature(runtimeMethod); + } + + internal MethodInfo RuntimeMethod { get; } + + internal Type ReplacementType { get; } + + internal bool IsSupported { get; } + + internal string Signature { get; } + } + + private static class ApiDiffGate + { + internal static IReadOnlyList Classify( + IEnumerable runtimeSignatures, + IEnumerable supportedSignatures, + IEnumerable replacementSignatures, + IReadOnlyDictionary unsupportedSignatures) + { + var errors = new List(); + var supported = new HashSet(supportedSignatures); + var replacements = new HashSet(replacementSignatures); + var runtime = new HashSet(runtimeSignatures); + + foreach (string signature in runtime) + { + if (supported.Contains(signature)) + { + if (!replacements.Contains(signature)) + { + errors.Add($"Missing controlled replacement for runtime signature '{signature}'."); + } + } + else if (unsupportedSignatures.TryGetValue(signature, out string reason)) + { + if (string.IsNullOrWhiteSpace(reason)) + { + errors.Add($"Allowlisted runtime signature '{signature}' must have a nonempty reason."); + } + } + else + { + errors.Add($"Unclassified runtime signature '{signature}'."); + } + } + + foreach (string signature in supported) + { + if (!runtime.Contains(signature)) + { + errors.Add($"Supported runtime signature '{signature}' is missing from this runtime."); + } + } + + foreach (string signature in unsupportedSignatures.Keys) + { + if (!runtime.Contains(signature)) + { + errors.Add($"Allowlisted runtime signature '{signature}' is missing from this runtime."); + } + } + + return errors; + } + } + } +} diff --git a/Tests/Tests.Rewriting/Types/TaskRewritingTests.cs b/Tests/Tests.Rewriting/Types/TaskRewritingTests.cs index 05109b7ce..17fb89506 100644 --- a/Tests/Tests.Rewriting/Types/TaskRewritingTests.cs +++ b/Tests/Tests.Rewriting/Types/TaskRewritingTests.cs @@ -1,6 +1,10 @@ // Copyright (c) Microsoft Corporation. // Licensed under the MIT License. +using System; +using System.Collections.Generic; +using System.IO; +using System.Threading; using System.Threading.Tasks; using Xunit; using Xunit.Abstractions; @@ -37,5 +41,376 @@ public void TestRewritingGenericTaskWhenAny() { Task.WhenAny(Task.FromResult(1)); } + +#if NET10_0_OR_GREATER + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAllWithCompilerSelectedSpanOverload() + { + Task.WhenAll(Task.CompletedTask, Task.CompletedTask); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAllWithSpan() + { + ReadOnlySpan tasks = new Task[] { Task.CompletedTask, Task.CompletedTask }; + Task.WhenAll(tasks); + } + + [Fact(Timeout = 5000)] + public void TestRewritingGenericTaskWhenAllWithSpan() + { + ReadOnlySpan> tasks = new Task[] { Task.FromResult(1), Task.FromResult(2) }; + Task.WhenAll(tasks); + } + + [Fact(Timeout = 5000)] + public void TestRewritingGenericTaskWhenAllWithCompilerSelectedSpanOverload() + { + Task.WhenAll(Task.FromResult(1), Task.FromResult(2)); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAnyWithSpan() + { + ReadOnlySpan tasks = new Task[] { Task.CompletedTask, Task.CompletedTask }; + Task.WhenAny(tasks); + } + + [Fact(Timeout = 5000)] + public void TestRewritingGenericTaskWhenAnyWithSpan() + { + ReadOnlySpan> tasks = new Task[] { Task.FromResult(1), Task.FromResult(2) }; + Task.WhenAny(tasks); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAllWithCompilerSelectedSpanOverload() + { + Task.WaitAll(Task.CompletedTask, Task.CompletedTask); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAllWithSpan() + { + ReadOnlySpan tasks = new Task[] { Task.CompletedTask, Task.CompletedTask }; + Task.WaitAll(tasks); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAllWithSpanSemantics() + { + this.Test(async () => + { + await Task.WhenAll([]); + await Task.WhenAll([Task.CompletedTask]); + await Task.WhenAll(Task.Run(() => { }), Task.Run(() => { })); + + int[] results = await Task.WhenAll([Task.FromResult(2), Task.FromResult(1)]); + Assert.Equal(new[] { 2, 1 }, results); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAllWithSpanFailureSemantics() + { + this.Test(async () => + { + await Assert.ThrowsAsync(() => + Task.WhenAll([Task.FromException(new InvalidOperationException())])); + + using var source = new CancellationTokenSource(); + source.Cancel(); + await Assert.ThrowsAnyAsync(() => + Task.WhenAll([Task.FromCanceled(source.Token)])); + + Assert.Throws(() => + { + _ = Task.WhenAll((ReadOnlySpan)new Task[] { null }); + }); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenAnyWithSpanSemantics() + { + this.Test(async () => + { + Task first = Task.CompletedTask; + Task genericFirst = Task.FromResult(1); + Assert.Same(first, await Task.WhenAny([first])); + Assert.Same(first, await Task.WhenAny(first, Task.Delay(1))); + Assert.Same(genericFirst, await Task.WhenAny([genericFirst, Task.FromResult(2)])); + Assert.Throws(() => + { + _ = Task.WhenAny((ReadOnlySpan)[]); + }); + Assert.Throws(() => + { + _ = Task.WhenAny((ReadOnlySpan)new Task[] { null }); + }); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAllWithSpanSemantics() + { + this.Test(() => + { + Task.WaitAll([]); + Task.WaitAll([Task.CompletedTask]); + Task.WaitAll(Task.Run(() => { }), Task.Run(() => { })); + Assert.Throws(() => + Task.WaitAll((ReadOnlySpan)new Task[] { null })); + Assert.Throws(() => + Task.WaitAll((ReadOnlySpan)new Task[] + { + Task.FromException(new InvalidOperationException()) + })); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenEachOverloads() + { + Task[] tasks = new[] { Task.CompletedTask }; + ReadOnlySpan taskSpan = tasks; + IEnumerable taskEnumerable = tasks; + _ = Task.WhenEach(tasks); + _ = Task.WhenEach(taskSpan); + _ = Task.WhenEach(taskEnumerable); + + Task[] genericTasks = new[] { Task.FromResult(1) }; + ReadOnlySpan> genericTaskSpan = genericTasks; + IEnumerable> genericTaskEnumerable = genericTasks; + _ = Task.WhenEach(genericTasks); + _ = Task.WhenEach(genericTaskSpan); + _ = Task.WhenEach(genericTaskEnumerable); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenEachCompletionOrder() + { + this.Test(async () => + { + var first = new TaskCompletionSource(); + var second = new TaskCompletionSource(); + await using IAsyncEnumerator enumerator = + Task.WhenEach(first.Task, second.Task).GetAsyncEnumerator(); + + second.SetResult(true); + Assert.True(await enumerator.MoveNextAsync()); + Assert.Same(second.Task, enumerator.Current); + + first.SetResult(true); + Assert.True(await enumerator.MoveNextAsync()); + Assert.Same(first.Task, enumerator.Current); + Assert.False(await enumerator.MoveNextAsync()); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingGenericTaskWhenEachCompletionStates() + { + this.Test(async () => + { + using var source = new CancellationTokenSource(); + source.Cancel(); + Task completed = Task.FromResult(1); + Task faulted = Task.FromException(new InvalidOperationException()); + Task canceled = Task.FromCanceled(source.Token); + var yielded = new List>(); + + await foreach (Task task in Task.WhenEach([completed, faulted, canceled])) + { + yielded.Add(task); + } + + Assert.Equal(3, yielded.Count); + Assert.Contains(completed, yielded); + Assert.Contains(faulted, yielded); + Assert.Contains(canceled, yielded); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenEachEmptyDuplicateAndEarlyStop() + { + this.Test(async () => + { + int count = 0; + await foreach (Task task in Task.WhenEach((Task[])[])) + { + count++; + } + + Assert.Equal(0, count); + + Task duplicate = Task.CompletedTask; + await foreach (Task task in Task.WhenEach([duplicate, duplicate])) + { + Assert.Same(duplicate, task); + count++; + } + + Assert.Equal(2, count); + + await foreach (Task task in Task.WhenEach([Task.CompletedTask, Task.CompletedTask])) + { + count++; + break; + } + + Assert.Equal(3, count); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWhenEachArgumentValidation() + { + // Assert the same validation semantics with and without a controlled runtime. + AssertWhenEachArgumentValidation(); + this.Test(() => AssertWhenEachArgumentValidation()); + } + + private static void AssertWhenEachArgumentValidation() + { + Assert.Throws(() => + { + _ = Task.WhenEach((IEnumerable)null); + }); + Assert.Throws(() => + { + _ = Task.WhenEach((IEnumerable>)null); + }); + Assert.Throws(() => + { + _ = Task.WhenEach((ReadOnlySpan)new Task[] { null }); + }); + Assert.Throws(() => + { + _ = Task.WhenEach((IEnumerable)new Task[] { null }); + }); + Assert.Throws(() => + { + _ = Task.WhenEach((ReadOnlySpan>)new Task[] { null }); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAsyncOverloads() + { + this.Test(async () => + { + using var source = new CancellationTokenSource(); + await Task.CompletedTask.WaitAsync(source.Token); + await Task.CompletedTask.WaitAsync(TimeSpan.Zero); + await Task.CompletedTask.WaitAsync(TimeSpan.Zero, source.Token); + await Task.CompletedTask.WaitAsync(TimeSpan.Zero, TimeProvider.System); + await Task.CompletedTask.WaitAsync(TimeSpan.Zero, TimeProvider.System, source.Token); + + Assert.Equal(1, await Task.FromResult(1).WaitAsync(source.Token)); + Assert.Equal(1, await Task.FromResult(1).WaitAsync(TimeSpan.Zero)); + Assert.Equal(1, await Task.FromResult(1).WaitAsync(TimeSpan.Zero, source.Token)); + Assert.Equal(1, await Task.FromResult(1).WaitAsync(TimeSpan.Zero, TimeProvider.System)); + Assert.Equal(1, await Task.FromResult(1).WaitAsync( + TimeSpan.Zero, TimeProvider.System, source.Token)); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAsyncTimeoutAndCancellation() + { + this.Test(async () => + { + var pending = new TaskCompletionSource(); + await Assert.ThrowsAsync(() => pending.Task.WaitAsync(TimeSpan.Zero)); + + using var source = new CancellationTokenSource(); + source.Cancel(); + await Assert.ThrowsAnyAsync(() => pending.Task.WaitAsync(source.Token)); + await Assert.ThrowsAsync(() => + Task.FromException(new InvalidOperationException()).WaitAsync(TimeSpan.FromMilliseconds(1))); + Assert.Throws(() => + { + _ = pending.Task.WaitAsync(TimeSpan.FromMilliseconds(-2)); + }); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskDelayWithSystemTimeProvider() + { + this.Test(async () => + { + await Task.Delay(TimeSpan.Zero, TimeProvider.System); + await Task.Delay(TimeSpan.Zero, TimeProvider.System, default); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingCustomTimeProviderIsExplicitlyUnsupported() + { + this.TestWithError(async () => + { + await Task.Delay(TimeSpan.Zero, new CustomTimeProvider()); + }, + expectedError: "Custom time providers are not supported in systematic testing."); + } + + [Fact(Timeout = 5000)] + public void TestRewritingWaitAsyncCustomTimeProviderIsExplicitlyUnsupported() + { + this.TestWithError(async () => + { + var pending = new TaskCompletionSource(); + await pending.Task.WaitAsync(TimeSpan.Zero, new CustomTimeProvider()); + }, + expectedError: "Custom time providers are not supported in systematic testing."); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAllWithEnumerable() + { + this.Test(() => + { + IEnumerable tasks = new[] { Task.CompletedTask, Task.CompletedTask }; + Task.WaitAll(tasks); + Task.WaitAll(tasks, default); + }); + } + + private sealed class CustomTimeProvider : TimeProvider + { + } + + [Fact(Timeout = 5000)] + public void TestNet10CompilerCallsAreRewrittenToControlledSignatures() + { + string assemblyPath = typeof(TaskRewritingTests).Assembly.Location; + string diff = File.ReadAllText(Path.ChangeExtension(assemblyPath, ".diff.json")); + Assert.Contains( + "System.Threading.Tasks.Task System.Threading.Tasks.Task::WhenAll(" + + "System.ReadOnlySpan`1)", + diff); + Assert.Contains( + "System.Threading.Tasks.Task " + + "Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task::WhenAll(" + + "System.ReadOnlySpan`1)", + diff); + Assert.Contains( + "System.Threading.Lock/Scope System.Threading.Lock::EnterScope()", + diff); + Assert.Contains( + "Microsoft.Coyote.Rewriting.Types.Threading.Lock::EnterScope(System.Threading.Lock)", + diff); + Assert.Contains( + "System.Threading.Tasks.Task::WhenEach(System.ReadOnlySpan`1)", + diff); + Assert.Contains( + "Microsoft.Coyote.Rewriting.Types.Threading.Tasks.Task::WhenEach(" + + "System.ReadOnlySpan`1)", + diff); + } +#endif } } diff --git a/Tests/Tests.Rewriting/Types/TaskWaitAsyncRewritingTests.cs b/Tests/Tests.Rewriting/Types/TaskWaitAsyncRewritingTests.cs new file mode 100644 index 000000000..4cf5132be --- /dev/null +++ b/Tests/Tests.Rewriting/Types/TaskWaitAsyncRewritingTests.cs @@ -0,0 +1,83 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +#if NET8_0_OR_GREATER +using System; +using System.Threading; +using System.Threading.Tasks; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.Rewriting.Tests +{ + public class TaskWaitAsyncRewritingTests : BaseRewritingTest + { + public TaskWaitAsyncRewritingTests(ITestOutputHelper output) + : base(output) + { + } + + [Fact(Timeout = 5000)] + public void TestRewritingNonGenericTaskWaitAsyncOverloads() + { + this.Test(async () => + { + using var source = new CancellationTokenSource(); + Task completed = Task.CompletedTask; + await completed.WaitAsync(source.Token); + await completed.WaitAsync(TimeSpan.Zero); + await completed.WaitAsync(TimeSpan.Zero, source.Token); + await completed.WaitAsync(TimeSpan.Zero, TimeProvider.System); + await completed.WaitAsync(TimeSpan.Zero, TimeProvider.System, source.Token); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingGenericTaskWaitAsyncOverloads() + { + this.Test(async () => + { + using var source = new CancellationTokenSource(); + Task completed = Task.FromResult(37); + Assert.Equal(37, await completed.WaitAsync(source.Token)); + Assert.Equal(37, await completed.WaitAsync(TimeSpan.Zero)); + Assert.Equal(37, await completed.WaitAsync(TimeSpan.Zero, source.Token)); + Assert.Equal(37, await completed.WaitAsync(TimeSpan.Zero, TimeProvider.System)); + Assert.Equal(37, await completed.WaitAsync(TimeSpan.Zero, TimeProvider.System, source.Token)); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAsyncTimeoutAndCancellation() + { + this.Test(async () => + { + var pending = new TaskCompletionSource(); + await Assert.ThrowsAsync(() => pending.Task.WaitAsync(TimeSpan.Zero)); + + using var source = new CancellationTokenSource(); + source.Cancel(); + await Assert.ThrowsAnyAsync(() => pending.Task.WaitAsync(source.Token)); + Assert.Throws(() => + { + _ = pending.Task.WaitAsync(TimeSpan.FromMilliseconds(-2), TimeProvider.System); + }); + }); + } + + [Fact(Timeout = 5000)] + public void TestRewritingTaskWaitAsyncPropagatesCompletionAndFaults() + { + this.Test(async () => + { + Assert.Equal(17, await Task.FromResult(17).WaitAsync( + TimeSpan.FromMilliseconds(10), TimeProvider.System)); + + var error = new InvalidOperationException("expected"); + await Assert.ThrowsAsync(() => + Task.FromException(error).WaitAsync(TimeSpan.FromMilliseconds(1), TimeProvider.System)); + }); + } + } +} +#endif diff --git a/Tests/Tests.Runtime/Tests.Runtime.csproj b/Tests/Tests.Runtime/Tests.Runtime.csproj index 22ff0298d..0a27f6e99 100644 --- a/Tests/Tests.Runtime/Tests.Runtime.csproj +++ b/Tests/Tests.Runtime/Tests.Runtime.csproj @@ -7,7 +7,7 @@ false false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020,xUnit1030,xUnit1031 @@ -19,8 +19,8 @@ - - + + diff --git a/Tests/Tests.Tools/Tests.Tools.csproj b/Tests/Tests.Tools/Tests.Tools.csproj index cacb71507..45251cfd9 100644 --- a/Tests/Tests.Tools/Tests.Tools.csproj +++ b/Tests/Tests.Tools/Tests.Tools.csproj @@ -7,7 +7,7 @@ false false false - $(NoWarn),1591 + $(NoWarn),1591,xUnit2020,xUnit1030,xUnit1031 @@ -19,8 +19,8 @@ - - + + diff --git a/Tests/compare-rewriting-diff-logs.ps1 b/Tests/compare-rewriting-diff-logs.ps1 index 03a23ebe5..aaa5bcb0d 100644 --- a/Tests/compare-rewriting-diff-logs.ps1 +++ b/Tests/compare-rewriting-diff-logs.ps1 @@ -1,9 +1,13 @@ # Copyright (c) Microsoft Corporation. # Licensed under the MIT License. +param( + [ValidateSet("net10.0", "net8.0")] + [string]$framework = "net10.0" +) + Import-Module $PSScriptRoot/../Scripts/common.psm1 -Force -$framework = "net8.0" $targets = [ordered]@{ "rewriting" = "Tests.Rewriting" "rewriting-helpers" = "Tests.Rewriting.Helpers" @@ -13,11 +17,16 @@ $targets = [ordered]@{ } $expected_hashes = [ordered]@{ - "rewriting" = "F5A50C959279CCC2A472B54B483D96488BD93C941B357F638C49B4B3462081E7" - "rewriting-helpers" = "DF8CF299C162ECA5392793BF5E3E6D7C8B61A75E029501ED6F41C1DD1AD3183B" - "testing" = "60F9D004CB61985FCFE111D2E25912124353FB3A97F25A75F301F5B647E7136B" - "actors" = "11AAFFA693116B24EB3EA152EE96757D8E9F7C57FFD3213ED02CDF1E9180D3D7" - "actors-testing" = "492B76D5ADE4E6EEA94A4AD1A37AD9DF911C81660600609FA1E9DF5D1B7AD860" + "net10.0|rewriting" = "1C099962B04E8F6574924BD6C67B15CE6C4411D747611C27F2F2D021FCAD3AC4" + "net10.0|rewriting-helpers" = "DF8CF299C162ECA5392793BF5E3E6D7C8B61A75E029501ED6F41C1DD1AD3183B" + "net10.0|testing" = "E04044B54F210C957AB927D274149573D9889FF50EFDD30E5C61829C77D1A354" + "net10.0|actors" = "4532F902A1C0A9D8F499D5D7512CEBF2E0D1AE83502B3BD2180E4897DC663963" + "net10.0|actors-testing" = "D11AFDFE4EA1D604423B07E650F5BC4495B04D70E48EA644D38387D3B2775716" + "net8.0|rewriting" = "075B580D1FC0F65D0AE49B616E1EC249B84392C377BBD3DCD740A86EFED8A8F0" + "net8.0|rewriting-helpers" = "DF8CF299C162ECA5392793BF5E3E6D7C8B61A75E029501ED6F41C1DD1AD3183B" + "net8.0|testing" = "DE0D083F5C4CB86697D27DEFB458F2253A1D655162BD4A6B2EF9D1E2021FD3E1" + "net8.0|actors" = "7E219081D30C11F60AC0689EA86E7F809795FFB07C07CA86B378DB6FBAF54349" + "net8.0|actors-testing" = "29D71EE8298B402FF3477D5EE89639C22B5295027B3C09EE366373DAE37A5D59" } Write-Comment -prefix "." -text "Comparing the test rewriting diff logs" -color "yellow" @@ -35,7 +44,7 @@ foreach ($kvp in $targets.GetEnumerator()) { $new = "$PSScriptRoot/$project/bin/$framework/Microsoft.Coyote.$($kvp.Value).diff.json" $new_hash = $(Get-FileHash $new).Hash Write-Comment -prefix "..." -text "Computed IL diff hash '$new_hash' for '$($kvp.Value)' project" - $expected_hash = $expected_hashes[$($kvp.Key)] + $expected_hash = $expected_hashes["$framework|$($kvp.Key)"] if ($new_hash -ne $expected_hash) { Write-Error "The '$($kvp.Value)' project's IL diff hash '$new_hash' is not the expected '$expected_hash'." $succeeded = $false diff --git a/Tests/get-rewriting-diff-logs.ps1 b/Tests/get-rewriting-diff-logs.ps1 index 8def4195e..4c7fa27ef 100644 --- a/Tests/get-rewriting-diff-logs.ps1 +++ b/Tests/get-rewriting-diff-logs.ps1 @@ -1,9 +1,13 @@ # Copyright (c) Microsoft Corporation. # Licensed under the MIT License. +param( + [ValidateSet("net10.0", "net8.0")] + [string]$framework = "net10.0" +) + Import-Module $PSScriptRoot/../Scripts/common.psm1 -Force -$framework = "net8.0" $targets = [ordered]@{ "rewriting" = "Tests.Rewriting" "rewriting-helpers" = "Tests.Rewriting.Helpers" diff --git a/Tools/CLI/Coyote.CLI.csproj b/Tools/CLI/Coyote.CLI.csproj index 21fe9a0d6..112f955f4 100644 --- a/Tools/CLI/Coyote.CLI.csproj +++ b/Tools/CLI/Coyote.CLI.csproj @@ -24,6 +24,10 @@ + + + + diff --git a/Tools/CoverageReportMerger/CoverageReportMerger.csproj b/Tools/CoverageReportMerger/CoverageReportMerger.csproj index ad4824b1c..12cb9e252 100644 --- a/Tools/CoverageReportMerger/CoverageReportMerger.csproj +++ b/Tools/CoverageReportMerger/CoverageReportMerger.csproj @@ -15,4 +15,8 @@ + + + + \ No newline at end of file diff --git a/Tools/Coyote/Coyote.csproj b/Tools/Coyote/Coyote.csproj index d886493b3..2d9906e5b 100644 --- a/Tools/Coyote/Coyote.csproj +++ b/Tools/Coyote/Coyote.csproj @@ -29,6 +29,13 @@ all + + + + + all + + diff --git a/docs/concepts/binary-rewriting.md b/docs/concepts/binary-rewriting.md index 31a82f46b..7b9be8dd6 100644 --- a/docs/concepts/binary-rewriting.md +++ b/docs/concepts/binary-rewriting.md @@ -26,6 +26,14 @@ To learn how to test your application after rewriting your binaries with Coyote, [here](../get-started/using-coyote.md), as well as check out our tutorial on [writing your first concurrency unit test](../tutorials/first-concurrency-unit-test.md). +### Choosing the right Coyote host + +Coyote ships a host for each supported .NET version. Rewriting injects references to the runtime of +the host that performs it, so you must run the host that matches the .NET major version targeted by +the assembly: use the `net8.0` Coyote host to rewrite a `net8.0` assembly and the `net10.0` host to +rewrite a `net10.0` assembly. If the versions do not match, `coyote rewrite` reports an error naming +both versions and leaves the assembly unmodified. + ### Configuration If you have multiple binaries to rewrite, then you should provide a JSON rewriting configuration @@ -106,6 +114,37 @@ you can already get tests up and running without requiring to mock every single experience pay-as-you-go. And our plan is that as partially-controlled exploration improves over time, you transparently also get better coverage without having to do much from your side. +### How timeouts are modeled + +The controlled scheduler serializes your program and decides itself when each operation runs, so it +does not measure wall-clock time. Rewritten synchronization APIs that accept a timeout therefore do +not treat that timeout as a source of nondeterminism during systematic testing: + +- A **finite non-zero** timeout is explored as if it was infinite, so the wait completes when the + operation that it is waiting for completes. Racing the wait against its timeout would instead + make every wait fail in some schedules, no matter how large the timeout is, reporting timeouts + that the program is not expected to observe and hiding the bugs that happen after the wait + succeeds. `Task.Wait`, `Task.WaitAll`, `Task.WaitAny`, `Task.WaitAsync`, `Monitor.Wait`, + `SemaphoreSlim.Wait`, `SemaphoreSlim.WaitAsync`, `WaitHandle.WaitOne`, `WaitHandle.WaitAll`, + `WaitHandle.WaitAny` and `Thread.Join` all follow this rule. The exception is `Lock.TryEnter`, + which reports a finite non-zero timeout as unsupported rather than blocking indefinitely on a + lock that its caller expects to give up on. +- If no operation can ever complete such a wait, then the runtime reports it as a **deadlock**, + which is how it reports any other wait that cannot be satisfied. +- Where the API can return without giving any other operation a chance to run first, a **zero** + timeout keeps its production meaning: `Task.WaitAsync` throws a `TimeoutException`, and + `SemaphoreSlim.Wait`, `SemaphoreSlim.WaitAsync`, `WaitHandle.WaitOne` and `Lock.TryEnter` report + that they did not acquire the resource. + +This policy does not change how cancellation is observed. Where the API takes a cancellation token +that Coyote controls, such as `Task.WaitAsync`, a wait with a finite timeout still completes as +canceled when the token is canceled, and a token that is already canceled when the wait starts +takes precedence over the timeout, exactly as it does in production. + +Systematic fuzzing is different: it executes the program on real threads and in real time, only +injecting delays in between operations. Timeouts there keep their wall-clock meaning and are +handled by the uncontrolled .NET runtime. + ### Quality of life improvements through rewriting Coyote will automatically rewrite certain parts of your test code (without changing the application diff --git a/global.json b/global.json index 8c70738ad..195fae797 100644 --- a/global.json +++ b/global.json @@ -1,5 +1,6 @@ { "sdk": { - "version": "8.0.404" + "version": "10.0.303", + "rollForward": "latestPatch" } }