diff --git a/regression/cbmc-concurrency/array1/main.c b/regression/cbmc-concurrency/array1/main.c new file mode 100644 index 00000000000..8574bbd66ff --- /dev/null +++ b/regression/cbmc-concurrency/array1/main.c @@ -0,0 +1,19 @@ +int data[2]; +unsigned sync; + +void thread() +{ + data[sync % 2] = 1; + __CPROVER_assert(data[sync % 2] == 1, "1"); +} + +int main() +{ + unsigned nondet; + sync = nondet; +__CPROVER_ASYNC_1: + thread(); + unsigned sync_value = sync; + data[(sync_value + 1) % 2] = 2; + __CPROVER_assert(data[(sync_value + 1) % 2] == 2, "2"); +} diff --git a/regression/cbmc-concurrency/array1/test.desc b/regression/cbmc-concurrency/array1/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc-concurrency/array1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 316a2dd5ace..9fff87a639d 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -117,10 +117,28 @@ void goto_symext::symex_assign( return; } + // We may end up reading (and writing) all components of an object composed + // of multiple fields. In such cases, we must do so atomically to avoid + // overwriting components modified by another thread. Note that this also + // implies multiple shared reads on the rhs being treated as atomic. + const bool maybe_divisible = + lhs.id() == ID_index || + (is_ssa_expr(lhs) && + state.field_sensitivity.is_divisible(to_ssa_expr(lhs), false)); + const bool need_atomic_section = maybe_divisible && + state.threads.size() > 1 && + state.atomic_section_id == 0; + + if(need_atomic_section) + symex_atomic_begin(state); + exprt::operandst lhs_if_then_else_conditions; symex_assignt{ shadow_memory, state, assignment_type, ns, symex_config, target} .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions); + + if(need_atomic_section) + symex_atomic_end(state); } }