[WIP] Concurrency with pointers#8917
Draft
tautschnig wants to merge 11 commits intodiffblue:developfrom
Draft
Conversation
Collaborator
tautschnig
commented
Mar 28, 2026
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
We cannot soundly handle pointer offsets that are shared across threads, and will reject this in future to avoid unsound verification results. Here, however, the pointer offsets are not actually shared, so we can safely mark them `__CPROVER_thread_local`.
…ed pointers Reading and writing pointers is not not itself unsound, only the interaction with value sets may cause unsound results. Hence, do not reject programs that never dereference a shared pointer. Fixes: diffblue#8714 Fixes: diffblue#7957
Shared pointers may be updated in yet-to-be-executed threads.
…current context Instead of throwing unsupported_operation_exceptiont when a shared pointer is dereferenced in a multi-threaded context, create a fresh concurrency::may_alias symbol of the appropriate pointed-to type. This symbol bypasses the value-set dereference and serves as a placeholder for the memory model to later create conditional aliasing constraints. Changes: - Add may_alias_pointer field and is_may_alias() helper to SSA_stept - Transform check_concurrency_soundness into find_shared_pointer_in_dereference which returns the shared symbol instead of throwing - In dereference_rec, when a shared pointer is detected, create a fresh may-alias symbol via get_fresh_aux_symbol and annotate it with the source pointer expression - Update regression tests that expected the old exception message
…ency events Modify the partial-order constraint generation to account for may-alias objects created during shared pointer dereferences in concurrent context. Key changes: - Store source pointer on symbolt::value instead of ID_C_class annotation so it survives SSA renaming (lookup by object name from symbol table) - In build_event_lists, add a second pass that distributes may-alias events to all type-compatible non-may-alias addresses in the address_map - Record address representatives (L1 ssa_exprt) for building alias conditions - Add alias_condition() method that builds pointer_object equality between the source pointer and address-of the target object - Guard write_serialization_external constraints with alias conditions - Guard read_from constraints with alias conditions (passed through to register_read_from_choice_symbol) - Guard from_read constraints with alias conditions - Skip init writes for may-alias addresses (their semantics are captured by aliasing constraints, not initialization) - Update regression test expectations for dirty_local1, malloc1, and global_pointer1/detect_unsoundness to reflect correct analysis results
Add three new regression tests exercising the may-alias object creation and constraint generation for shared pointer dereferences: - may_alias1: Tests the issue example (allocator pattern with __CPROVER_allocate). Verifies VERIFICATION SUCCESSFUL with proper synchronization via assumes. - may_alias2: Tests reading through a shared pointer where another thread writes the value and sets the pointer. Verifies no exception is thrown. - may_alias3: Tests a case where another thread changes a shared pointer to point to a different object. Verifies no exception and the old 'unsound' message does not appear. All three tests verify that the old 'pointer handling for concurrency is unsound' exception no longer occurs.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The rf-some constraint (which says 'a read must read from at least one write') was generated per-address without alias guards. When a may-alias read was added to multiple addresses (e.g., val1 and val2), it got separate rf-some constraints for each, forcing it to read from ALL addresses simultaneously. Since a read can only read from one write, this made the constraints unsatisfiable, causing the solver to make the guard false and assertions vacuously true. Fix by guarding the rf-some constraint with the alias condition: the may-alias read only needs to read from writes at address A if the source pointer actually points to A. Also fix the source pointer stored for alias conditions to use the L2-renamed version, which is properly constrained by the memory model's read-from relation for the pointer variable itself. Background: the partial-order encoding follows Alglave/Kroening/ Tautschnig CAV 2013 'Partial Orders for Efficient Bounded Model Checking of Concurrent Software'. The rf-some constraint corresponds to Section 4.2's requirement that each read maps to at least one write via the read-from relation. See may_alias_soundness.md for a formal soundness argument. Additional cleanup: - Extract is_may_alias_step() and is_may_alias_address() helpers - Remove unused may_alias_pointer field from SSA_stept - Add detailed comments referencing the CAV 2013 paper to all constraint generation functions (read_from, write_serialization, from_read) - Add soundness regression test that verifies a real concurrent bug IS detected (assertion correctly fails when pointer aliasing makes the property false) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Local pointers assigned from shared sources (e.g., int *local = shared_ptr) were not detected as needing may-alias treatment, causing missed bugs. Fix by querying the value set when dereferencing a local pointer symbol: if any of the pointer's possible targets is a shared global variable, treat the dereference as shared and create a may-alias object. The check excludes: - Struct member accesses (to avoid false positives from thread arguments) - Failed symbols (internal CBMC objects) - Dynamic objects (malloc'd memory is shared by design but doesn't need may-alias treatment — the value-set dereference handles it correctly) - __spawned_thread parameters (thread-local copies of pthread_create args) Root cause of thread_chain_posix2 regression: __spawned_thread parameters are not marked thread_local, and constant propagation substitutes them into pointer expressions. Dynamic objects from malloc are also not thread_local. Both caused false may-alias triggers. Fixed by excluding __spawned_thread symbols from the direct check and dynamic objects from the indirect (value-set) check. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…aints When a pointer of one type (e.g., int*) points to an object of a different type (e.g., unsigned int, or char accessing an int), the rf-val constraint needs to reinterpret the write value as the read's type. Use byte_extract (the canonical CBMC mechanism for memory reinterpretation) instead of typecast_exprt. byte_extract handles: - Same-width types (simplifier reduces to typecast): int/unsigned - Different-width types (proper byte extraction): char* into int - The expression simplifier optimizes away trivial cases Remove the same-size type restriction from the address distribution: may-alias events are now distributed to all addresses with known bit width. This is more general and correct — the byte_extract in the rf-val constraint handles any type combination. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add a --refine-concurrency option that disables MiniSAT's SimpSolver (which eliminates variables during preprocessing) to enable future incremental concurrency constraint solving. This follows the same pattern as --refine-strings (see tautschnig/array-fixes branch). The memory model base class gains: - prepare(): builds event lists and clock types - add_init_writes_only(): adds init writes without full event lists - add_stage(): adds constraints for a specific refinement stage (READ_FROM, PROGRAM_ORDER, WRITE_SERIALIZATION, FROM_READ) Currently all constraints are added upfront (the incremental loop requires careful handling of init writes that must be in the equation before solver conversion). The disabled simplifier and staged API provide the infrastructure for true incremental solving in the future. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8917 +/- ##
=========================================
Coverage 80.41% 80.41%
=========================================
Files 1703 1704 +1
Lines 188398 188565 +167
Branches 73 73
=========================================
+ Hits 151496 151635 +139
- Misses 36902 36930 +28 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.