Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: thread-safety issue in the runtime #1780

Merged
merged 15 commits into from
Feb 19, 2022

Conversation

fabiomadge
Copy link
Collaborator

@fabiomadge fabiomadge commented Feb 3, 2022

Fixes #1454

@fabiomadge fabiomadge changed the title fix:gh 1454 fix: Feb 3, 2022
@fabiomadge fabiomadge changed the title fix: fix: thread-safety issue in the runtime Feb 3, 2022
@fabiomadge fabiomadge marked this pull request as draft February 3, 2022 06:12
@fabiomadge fabiomadge self-assigned this Feb 3, 2022
}

[Fact(Timeout = 5000)]
public void RunCoyoteTest() {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm happy to say I'm able to run this test locally myself (after doing a dotnet tool restore), but it passes even if I revert your fix below. I CAN reproduce the problem by only commenting out all but two tasks and setting a breakpoint on the elmts = ComputeElements(); line of the ImmutableElements getter and then debugging the ConcatSequence test directly through Rider: having two threads ready to go on that line pretty consistently leads to NullReferenceExceptions once I resume execution.

My hope was that Coyote would be able to definitively reproduce the bug first, since it's deterministically testing many thread interleavings. We should either find a simple enough Coyote test that reveals the bug, or not bother with Coyote at all.

Source/DafnyRuntime/DafnyRuntime.cs Show resolved Hide resolved
@fabiomadge fabiomadge marked this pull request as ready for review February 18, 2022 22:16
Source/DafnyRuntime/DafnyRuntime.cs Show resolved Hide resolved
Source/DafnyRuntime/DafnyRuntime.cs Show resolved Hide resolved
@robin-aws robin-aws dismissed their stale review February 18, 2022 23:34

Not confident enough to approve, but don't want to block while away

Copy link
Member

@cpitclaudel cpitclaudel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧵🧵🧵

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Lazy sequence concatenation in Java runtime is not thread-safe
3 participants