Partial-order concurrency: permit data races

regression/cbmc-concurrency/memory_barrier2/main.c

@@ -7,6 +7,7 @@ int x; // variable to test mutual exclusion
 volatile int flag1 = 0, flag2 = 0; // boolean flags
 
 void* thr1(void * arg) { // frontend produces 12 transitions from this thread. It would be better if it would produce only 8!
+  __CPROVER_atomic_begin();
   flag1 = 1;
   turn = 1;
 #ifdef __GNUC__
@@ -20,9 +21,11 @@ void* thr1(void * arg) { // frontend produces 12 transitions from this thread. I
   assert(x<=0);
   // end: critical section
   flag1 = 0;
+  __CPROVER_atomic_end();
 }
 
 void* thr2(void * arg) {
+  __CPROVER_atomic_begin();
   flag2 = 1;
   turn = 0;
 #ifdef __GNUC__
@@ -36,6 +39,7 @@ void* thr2(void * arg) {
   assert (x>=1);
   // end: critical section
   flag2 = 0;
+  __CPROVER_atomic_end();
 }
 
 int main()

regression/cbmc-concurrency/memory_barrier2/msvc.c

@@ -5,7 +5,9 @@ volatile int flag1 = 0, flag2 = 0;
 void *thr1(void *arg)
 {
   flag1 = 1;
+  __CPROVER_atomic_begin();
   turn = 1;
+  __CPROVER_atomic_end();
   __asm { mfence; }
   __CPROVER_assume(!(flag2 == 1 && turn == 1));
   x = 0;
@@ -16,7 +18,9 @@ void *thr1(void *arg)
 void *thr2(void *arg)
 {
   flag2 = 1;
+  __CPROVER_atomic_begin();
   turn = 0;
+  __CPROVER_atomic_end();
   __asm { mfence; }
   __CPROVER_assume(!(flag1 == 1 && turn == 0));
   x = 1;

src/ansi-c/library/pthread_lib.c

@@ -356,7 +356,9 @@ __CPROVER_HIDE:;
   if((unsigned long)thread>__CPROVER_next_thread_id) return ESRCH;
   if((unsigned long)thread==__CPROVER_thread_id) return EDEADLK;
   if(value_ptr!=0) (void)**(char**)value_ptr;
+  __CPROVER_atomic_begin();
   __CPROVER_assume(__CPROVER_threads_exited[(unsigned long)thread]);
+  __CPROVER_atomic_end();
 
   return 0;
 }
@@ -604,7 +606,9 @@ __CPROVER_HIDE:;
       __CPROVER_thread_key_dtors[i](key);
   }
 #endif
+  __CPROVER_atomic_begin();
   __CPROVER_threads_exited[this_thread_id] = 1;
+  __CPROVER_atomic_end();
 }
 
 /* FUNCTION: pthread_create */

src/goto-symex/memory_model.cpp

@@ -48,6 +48,7 @@ void memory_model_baset::read_from(symex_target_equationt &equation)
 
   for(const auto &address : address_map)
   {
+    std::size_t r_w_property_counter = 0;
     for(const auto &read_event : address.second.reads)
     {
       exprt::operandst rf_choice_symbols;
@@ -60,7 +61,7 @@ void memory_model_baset::read_from(symex_target_equationt &equation)
         if(!po(read_event, write_event))
         {
           rf_choice_symbols.push_back(register_read_from_choice_symbol(
-            read_event, write_event, equation));
+            read_event, write_event, equation, r_w_property_counter));
         }
       }
 
@@ -83,7 +84,8 @@ void memory_model_baset::read_from(symex_target_equationt &equation)
 symbol_exprt memory_model_baset::register_read_from_choice_symbol(
   const event_it &r,
   const event_it &w,
-  symex_target_equationt &equation)
+  symex_target_equationt &equation,
+  std::size_t &property_counter)
 {
   symbol_exprt s = nondet_bool_symbol("rf");
 
@@ -106,6 +108,16 @@ symbol_exprt memory_model_baset::register_read_from_choice_symbol(
     // if r reads from w, then w must have happened before r
     add_constraint(
       equation, implies_exprt{s, before(w, r)}, "rf-order", r->source);
+#if 0
+    notequal_exprt ne{clock(w, axiomt::AX_PROPAGATION), clock(r, axiomt::AX_PROPAGATION)};
+    const std::string sym_name = id2string(r->ssa_lhs.get_identifier());
+    equation.assertion(
+      simplify_expr(and_exprt{w->guard, r->guard}, ns),
+      ne,
+      sym_name + ".r_w_data_race." + std::to_string(++property_counter),
+      "read/write data race on " + sym_name,
+      r->source);
+#endif
   }
 
   return s;

src/goto-symex/memory_model.h

@@ -50,11 +50,14 @@ class memory_model_baset : public partial_order_concurrencyt
   /// \param r: read event
   /// \param w: write event
   /// \param equation: symex equation where the new constraints should be added
+  /// \param property_counter: used and updated to count the number of
+  ///   read/write data race assertions
   /// \return the new choice symbol
   symbol_exprt register_read_from_choice_symbol(
     const event_it &r,
     const event_it &w,
-    symex_target_equationt &equation);
+    symex_target_equationt &equation,
+    std::size_t &property_counter);
 
   // maps thread numbers to an event list
   typedef std::map<unsigned, event_listt> per_thread_mapt;

src/goto-symex/memory_model_sc.cpp

@@ -208,6 +208,9 @@ void memory_model_sct::write_serialization_external(
     // This is quadratic in the number of writes
     // per address. Perhaps some better encoding
     // based on 'places'?
+#if 0
+    std::size_t w_w_data_race_property_counter = 0;
+#endif
     for(event_listt::const_iterator
         w_it1=a_rec.writes.begin();
         w_it1!=a_rec.writes.end();
@@ -225,23 +228,31 @@ void memory_model_sct::write_serialization_external(
            (*w_it2)->source.thread_nr)
           continue;
 
-        // ws is a total order, no two elements have the same rank
-        // s -> w_evt1 before w_evt2; !s -> w_evt2 before w_evt1
-
-        symbol_exprt s=nondet_bool_symbol("ws-ext");
-
-        // write-to-write edge
-        add_constraint(
-          equation,
-          implies_exprt(s, before(*w_it1, *w_it2)),
-          "ws-ext",
-          (*w_it1)->source);
+        // ws is a total order, no two elements in distinct atomic sections have
+        // the same rank
+        DATA_INVARIANT(
+          (*w_it1)->atomic_section_id == 0 ||
+          (*w_it1)->atomic_section_id != (*w_it2)->atomic_section_id,
+          "non-atomic writes in distinct threads cannot belong to the same "
+          "atomic section");
 
-        add_constraint(
-          equation,
-          implies_exprt(not_exprt(s), before(*w_it2, *w_it1)),
-          "ws-ext",
-          (*w_it1)->source);
+        if((*w_it1)->atomic_section_id != 0 && (*w_it2)->atomic_section_id != 0)
+        {
+          notequal_exprt ne{clock(*w_it1, axiomt::AX_PROPAGATION), clock(*w_it2, axiomt::AX_PROPAGATION)};
+          equation.constraint(ne, "ws-ext", (*w_it1)->source);
+        }
+        else
+        {
+#if 0
+           notequal_exprt ne{clock(*w_it1, axiomt::AX_PROPAGATION), clock(*w_it2, axiomt::AX_PROPAGATION)};
+          equation.assertion(
+            simplify_expr(and_exprt{(*w_it1)->guard, (*w_it2)->guard}, ns),
+            ne,
+            id2string(a_it->first) + ".w_w_data_race." + std::to_string(++w_w_data_race_property_counter),
+            "write/write data race on " + id2string(a_it->first),
+            (*w_it1)->source);
+#endif
+        }
       }
     }
   }

src/goto-symex/memory_model_sc.h

@@ -38,7 +38,7 @@ class memory_model_sct:public memory_model_baset
     const per_thread_mapt &per_thread_map);
   void program_order(symex_target_equationt &equation);
   void from_read(symex_target_equationt &equation);
-  void write_serialization_external(symex_target_equationt &equation);
+  virtual void write_serialization_external(symex_target_equationt &equation);
 };
 
 #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_SC_H

src/goto-symex/memory_model_tso.cpp

@@ -164,3 +164,78 @@ void memory_model_tsot::program_order(
     }
   }
 }
+
+void memory_model_tsot::write_serialization_external(
+  symex_target_equationt &equation)
+{
+  for(address_mapt::const_iterator
+      a_it=address_map.begin();
+      a_it!=address_map.end();
+      a_it++)
+  {
+    const a_rect &a_rec=a_it->second;
+
+    // This is quadratic in the number of writes
+    // per address. Perhaps some better encoding
+    // based on 'places'?
+#if 0
+    std::size_t w_w_data_race_property_counter = 0;
+#endif
+    for(event_listt::const_iterator
+        w_it1=a_rec.writes.begin();
+        w_it1!=a_rec.writes.end();
+        ++w_it1)
+    {
+      event_listt::const_iterator next=w_it1;
+      ++next;
+
+      for(event_listt::const_iterator w_it2=next;
+          w_it2!=a_rec.writes.end();
+          ++w_it2)
+      {
+        // external?
+        if((*w_it1)->source.thread_nr==
+           (*w_it2)->source.thread_nr)
+          continue;
+
+        // ws is a total order, no two elements in distinct atomic sections have
+        // the same rank
+        DATA_INVARIANT(
+          (*w_it1)->atomic_section_id == 0 ||
+          (*w_it1)->atomic_section_id != (*w_it2)->atomic_section_id,
+          "non-atomic writes in distinct threads cannot belong to the same "
+          "atomic section");
+
+        if((*w_it1)->atomic_section_id != 0 && (*w_it2)->atomic_section_id != 0)
+        {
+          symbol_exprt s=nondet_bool_symbol("ws-ext");
+
+          // write-to-write edge
+          add_constraint(
+            equation,
+            implies_exprt(s, before(*w_it1, *w_it2)),
+            "ws-ext",
+            (*w_it1)->source);
+
+          add_constraint(
+            equation,
+            implies_exprt(not_exprt(s), before(*w_it2, *w_it1)),
+            "ws-ext",
+            (*w_it1)->source);
+        }
+        else
+        {
+#if 0
+           notequal_exprt ne{clock(*w_it1, axiomt::AX_PROPAGATION), clock(*w_it2, axiomt::AX_PROPAGATION)};
+          equation.assertion(
+            simplify_expr(and_exprt{(*w_it1)->guard, (*w_it2)->guard}, ns),
+            ne,
+            id2string(a_it->first) + ".w_w_data_race." + std::to_string(++w_w_data_race_property_counter),
+            "write/write data race on " + id2string(a_it->first),
+            (*w_it1)->source);
+#endif
+        }
+      }
+    }
+  }
+}

src/goto-symex/memory_model_tso.h

@@ -30,6 +30,7 @@ class memory_model_tsot:public memory_model_sct
     partial_order_concurrencyt::event_it e1,
     partial_order_concurrencyt::event_it e2) const;
   void program_order(symex_target_equationt &equation);
+  void write_serialization_external(symex_target_equationt &equation) override;
 };
 
 #endif // CPROVER_GOTO_SYMEX_MEMORY_MODEL_TSO_H