dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Published 20 hours ago • verified publisher icon dafny-lang

Unstable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long

Open keyboardDrummer opened this issue 1 year ago • 9 comments
trafficstars

https://github.com/dafny-lang/dafny/actions/runs/9221662857/job/25371200992?pr=5484

keyboardDrummer avatar May 24 '24 10:05 keyboardDrummer

Log shows DafnyTestGeneration.Test was taking 52 minutes while locally it takes only 12 seconds, so it seems one of the tests stalled.

keyboardDrummer avatar May 27 '24 16:05 keyboardDrummer

~Comparing with a successful run, the cancelled run does finish all the tests successfully and none of the tests take very long. It seems as if the run gets stuck on winding down the testing.~

Contrary to the above, it does seem like a successful run finished more tests. The last passing test on a failed run is the NoInlining one. A successful run then still does:

  Passed DafnyTestGeneration.Test.Various.NoInlining(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.InliningRecursion(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.NestedInlining(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.Oracles(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [715 ms]
  Passed DafnyTestGeneration.Test.Various.TypePolymorphism(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.NoDeadCode(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [229 ms]
  Passed DafnyTestGeneration.Test.Various.FunctionCallInAMethodTranslation(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.Inlining(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.FunctionToMethodTranslation(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.Inlining(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.FunctionToMethodTranslation(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [715 ms]
  Passed DafnyTestGeneration.Test.Various.RecursivelyExtractDatatypeFields(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [2 s]
  Passed DafnyTestGeneration.Test.Various.FunctionMethodShortCircuit(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
  Passed DafnyTestGeneration.Test.Various.NonNullableObjects(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [685 ms]
  Passed DafnyTestGeneration.Test.Various.DeadCode(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [1 s]
[xUnit.net 00:01:12.32]   Finished:    DafnyTestGeneration.Test
  Passed DafnyTestGeneration.Test.Various.MethodWithNoVerificationGoal(optionSettings: [Action`1 { Method = Void <OptionSettings>b__1_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [674 ms]

Test Run Successful.
Total tests: 70
     Passed: 70

Possibly it's the InliningRecursion test that does not terminate.

keyboardDrummer avatar May 28 '24 08:05 keyboardDrummer

Seems like I'm hitting a related issue here: https://github.com/dafny-lang/dafny/actions/runs/9309791107/job/25627512636?pr=5506

MikaelMayer avatar May 31 '24 16:05 MikaelMayer 

The active test run was aborted. Reason: Test host process crashed
Data collector 'Blame' message: The specified inactivity time of 5 minutes has elapsed. Collecting hang dumps from testhost and its child processes.

Test Run Aborted.
Total tests: Unknown
     Passed: 61
 Total time: 6.0727 Minutes
Results File: /home/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/_fv-az1384-553_[202](https://github.com/dafny-lang/dafny/actions/runs/9387305957/job/25850793719?pr=5512#step:14:203)4-06-05_16_21_26.trx

The active Test Run was aborted because the host process exited unexpectedly. Please inspect the call stack above, if available, to get more information about where the exception originated from.
The test running when the crash occurred: 
DafnyTestGeneration.Test.WarningTests.UnsupportedInputTypeRecursive2

keyboardDrummer avatar Jun 06 '24 08:06 keyboardDrummer

Another one today https://github.com/dafny-lang/dafny/actions/runs/9455927389/job/26054080761?pr=5440

[createdump] Gathering state for process 20882 
[createdump] Writing full dump to file /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/b16f0746-9c1f-4b3e-80be-a28f8e7c3db0/dotnet_20882_20240611T024202_hangdump.dmp
[createdump] Written 3152777736 bytes (769721 pages) to core file
[createdump] Target process is alive
[createdump] Dump successfully written
The active test run was aborted. Reason: Test host process crashed
Data collector 'Blame' message: The specified inactivity time of 5 minutes has elapsed. Collecting hang dumps from testhost and its child processes.

Test Run Aborted.
Total tests: Unknown
     Passed: 49
 Total time: 6.9835 Minutes
Results File: /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/_Mac-1718069859867_2024-06-11_02_36_38.trx

The active Test Run was aborted because the host process exited unexpectedly. Please inspect the call stack above, if available, to get more information about where the exception originated from.
The test running when the crash occurred: 
DafnyTestGeneration.Test.Various.PathBasedTests

This test may, or may not be the source of the crash.

Attachments:
  /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/434fd35d-8e8e-431b-8984-fc0f6[103](https://github.com/dafny-lang/dafny/actions/runs/9455927389/job/26054080761?pr=5440#step:14:104)e9d4/dotnet_20882_20240611T024202_hangdump.dmp
  /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/434fd35d-8e8e-431b-8984-fc0f6103e9d4/Sequence_c9d3d8ed97ff4b5782f0e2f25c7f5827.xml
  /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/434fd35d-8e8e-431b-8984-fc0f6103e9d4/coverage.cobertura.xml

MikaelMayer avatar Jun 11 '24 17:06 MikaelMayer

@MikaelMayer I'm not working on this. Next step is finding someone to work on resolving it.

keyboardDrummer avatar Jun 12 '24 09:06 keyboardDrummer

New run exhibited that as well, preventing a PR to be merged: https://github.com/dafny-lang/dafny/actions/runs/9469813194/job/26089359440?pr=5440 Relevant extract:

[xUnit.net 00:00:52.05]     DafnyTestGeneration.Test.Collections.Tuples(optionSettings: [Action`1 { Method = Void <OptionSettings>b__5_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [FAIL]
[xUnit.net 00:00:52.05]       System.Threading.Tasks.TaskCanceledException : A task was canceled.
[xUnit.net 00:00:52.05]       Stack Trace:
[xUnit.net 00:00:52.06]         /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/Collections.cs(44,0): at DafnyTestGeneration.Test.Collections.Tuples(List`1 optionSettings)
[xUnit.net 00:00:52.06]         --- End of stack trace from previous location ---
[xUnit.net 00:00:52.06]       Output:
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(11,2)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(2,76):initialstate
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,15)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,29)#thenBranch
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,15)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,29)#thenBranch
[xUnit.net 00:00:52.06]         // Constructing the test for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12))...
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(11,2)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(2,76):initialstate
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,15)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,29)#thenBranch
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,15)
[xUnit.net 00:00:52.06]         // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,29)#thenBranch
[xUnit.net 00:00:52.06]         // Constructing the test for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16))...
[xUnit.net 00:00:52.06]         // No test is generated for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,24)#elseBranch) because the verifier proved that no inputs could cause this location to be visited.
  Failed DafnyTestGeneration.Test.Collections.Tuples(optionSettings: [Action`1 { Method = Void <OptionSettings>b__5_0(Microsoft.Dafny.DafnyOptions), Target = <>c { ... } }]) [50 s]
  Error Message:
   System.Threading.Tasks.TaskCanceledException : A task was canceled.
  Stack Trace:
     at DafnyTestGeneration.Test.Collections.Tuples(List`1 optionSettings) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/Collections.cs:line 44
--- End of stack trace from previous location ---
  Standard Output Messages:
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(11,2)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(2,76):initialstate
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,15)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,29)#thenBranch
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,15)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,29)#thenBranch
 // Constructing the test for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(10,12))...
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(11,2)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(2,76):initialstate
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,15)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(5,29)#thenBranch
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,15)
 // Test SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16)) covers /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,29)#thenBranch
 // Constructing the test for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(8,16))...
 // No test is generated for SimpleTest.tuple (/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/parseUtils.dfy(7,24)#elseBranch) because the verifier proved that no inputs could cause this location to be visited.

MikaelMayer avatar Jun 13 '24 01:06 MikaelMayer

Another instance yesterday. https://github.com/dafny-lang/dafny/actions/runs/9492186658/job/26158899590?pr=5440

[createdump] Gathering state for process 22173 
[createdump] Writing full dump to file /var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/18b4ae11-4805-4d68-8fcf-26a456f4aedc/dotnet_22173_20240613T015851_hangdump.dmp
[createdump] Written 3515724376 bytes (858331 pages) to core file
[createdump] Target process is alive
[createdump] Dump successfully written
The active test run was aborted. Reason: Test host process crashed
Data collector 'Blame' message: The specified inactivity time of 5 minutes has elapsed. Collecting hang dumps from testhost and its child processes.

Test Run Aborted.
Total tests: Unknown
     Passed: 57
     Failed: 1
 Total time: 7.8861 Minutes
Results File: /Users/runner/work/dafny/dafny/dafny/Source/DafnyTestGeneration.Test/TestResults/_Mac-1718240500761_2024-06-13_01_52_49.trx

The active Test Run was aborted because the host process exited unexpectedly. Please inspect the call stack above, if available, to get more information about where the exception originated from.
The test running when the crash occurred: 
DafnyTestGeneration.Test.WarningTests.UnsupportedInputTypeClass

This test may, or may not be the source of the crash.

MikaelMayer avatar Jun 13 '24 12:06 MikaelMayer

I found that I could at least reproduce the testing process locking up locally, by using Rider's "Run Selected Tests Until Failure" feature and letting it loop for perhaps a dozen runs. Unfortunately using "Debug Selected Tests Until Failure" so that I could debug thread state when it locks up hasn't been effective, since I haven't been able to reproduce it in that mode yet. I suspect this is because the Run mode uses the default parallelism, but Debug only runs tests sequentially (and I haven't yet found a way to override that).

Given that, as a stopgap it may be worth configuring the DafnyTestGeneration.Test project to always runs tests serially with [assembly: CollectionBehavior(DisableTestParallelization = true)] (https://xunit.net/docs/running-tests-in-parallel), if that might at least reduce the chances of locking up in CI.

robin-aws avatar Jun 13 '24 19:06 robin-aws