Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Feb 2, 2023

While debugging thread-modular witness validation, I implemented a special case for calloc with count 1, such that it avoids an intermediate array, which we cannot output invariants for. (Also committed here to demonstrate the issue.)

Surprisingly, this broke some zstd thread pool tests since additional races appeared. This PR contains further minimizations of the zstd thread pool example. Somehow the unsoundness appears to be that if there's an extra array domain in between, then accesses from free disappear altogether.

@sim642
Copy link
Member Author

sim642 commented Aug 2, 2023

Everything split between #1089 and #1124.

@sim642 sim642 closed this Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants