Merge pull request #6122 from tautschnig/concurrency-dirty-2

Dirty locals copied across threads require program-order constraints

Author: tautschnig

regression/cbmc-concurrency/dirty_local3/test-local.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 -Dlocals_bug
 ^EXIT=0$
@@ -7,12 +7,6 @@ main.c
 --
 ^warning: ignoring
 --
-There is a need for further debugging around copying local objects in
-the procedure spawning threads as we generate the following non-sensical
-constraint:
-// 28 file regression/cbmc-concurrency/dirty_local3/main.c line 3 function worker
-(57) CONSTRAINT(z!1@0#2 == z!1@0 || !choice_rf0)
-                ^^^^^^^^^^^^^^^^
-                comparison of L2 and L1 SSA symbols
-// 28 file regression/cbmc-concurrency/dirty_local3/main.c line 3 function worker
-(58) CONSTRAINT(choice_rf0)
+We previously missed SHARED_WRITE events in program order in a newly-spawned
+thread for dirty locals, resulting in spurious failures as reading from initial
+values seemed possible.

src/goto-symex/symex_start_thread.cpp

@@ -40,7 +40,7 @@ void goto_symext::symex_start_thread(statet &state)
     instruction.get_target();
 
   // put into thread vector
-  std::size_t t=state.threads.size();
+  const std::size_t new_thread_nr = state.threads.size();
   state.threads.push_back(statet::threadt(guard_manager));
   // statet::threadt &cur_thread=state.threads[state.source.thread_nr];
   statet::threadt &new_thread=state.threads.back();
@@ -54,6 +54,8 @@ void goto_symext::symex_start_thread(statet &state)
   new_thread.abstract_events=&(target.new_thread(cur_thread.abstract_events));
   #endif
 
+  const std::size_t current_thread_nr = state.source.thread_nr;
+
   // create a copy of the local variables for the new thread
   framet &frame = state.call_stack().top();
 
@@ -72,7 +74,8 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt lhs(pair.second.first.get_original_expr());
 
     // get L0 name for current thread
-    const renamedt<ssa_exprt, L0> l0_lhs = symex_level0(std::move(lhs), ns, t);
+    const renamedt<ssa_exprt, L0> l0_lhs =
+      symex_level0(std::move(lhs), ns, new_thread_nr);
     const irep_idt &l0_name = l0_lhs.get().get_identifier();
     std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
     CHECK_RETURN(l1_index == 0);
@@ -93,7 +96,20 @@ void goto_symext::symex_start_thread(statet &state)
     symex_assignt{
       state, symex_targett::assignment_typet::HIDDEN, ns, symex_config, target}
       .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
+    const exprt l2_lhs = state.rename(lhs_l1, ns).get();
     state.record_events.pop();
+
+    // record a shared write in the new thread
+    if(
+      state.write_is_shared(lhs_l1, ns) ==
+        goto_symex_statet::write_is_shared_resultt::SHARED &&
+      is_ssa_expr(l2_lhs))
+    {
+      state.source.thread_nr = new_thread_nr;
+      target.shared_write(
+        state.guard.as_expr(), to_ssa_expr(l2_lhs), 0, state.source);
+      state.source.thread_nr = current_thread_nr;
+    }
   }
 
   // initialize all variables marked thread-local
@@ -112,7 +128,7 @@ void goto_symext::symex_start_thread(statet &state)
     ssa_exprt lhs(symbol.symbol_expr());
 
     // get L0 name for current thread
-    lhs.set_level_0(t);
+    lhs.set_level_0(new_thread_nr);
 
     exprt rhs=symbol.value;
     if(rhs.is_nil())