edits: add comments to demonstrate the found bugs and bug injections

[model-checker-benchmarks.git] / seqlock / seqlock.cc

diff --git a/seqlock/seqlock.cc b/seqlock/seqlock.cc
index 16298bd04baa8010463ce8047a258b93c1c53754..ca4a55c0823e676dab31fab07f9d75d137894252 100644 (file)
--- a/seqlock/seqlock.cc
+++ b/seqlock/seqlock.cc
@@ -13,9 +13,10 @@ seqlock::seqlock() {
 
 void seqlock::read(int *data1, int *data2) {
        while (true) {
-               // XXX: This cannot be detected unless when we only have a single data
-               // varaible since that becomes a plain load/store. However, when we have
-               // multiple data pieces, we will detect the inconsitency of the data.
+        // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
+        // "memory_order_relaxed", run "make" to recompile, and then run:
+        // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
+
                /**********    Detected Correctness (testcase1)    **********/
                int old_seq = _seq.load(memory_order_acquire); // acquire
                if (old_seq % 2 == 1) {
@@ -24,10 +25,13 @@ void seqlock::read(int *data1, int *data2) {
         }
        
                // Acquire ensures that the second _seq reads an update-to-date value
-               /**********    Detected Correctness (testcase1)    **********/
                *data1 = _data1.load(memory_order_relaxed);
                *data2 = _data2.load(memory_order_relaxed);
                /** @OPClearDefine: true */
+
+        // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
+        // "memory_order_relaxed", run "make" to recompile, and then run:
+        // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
                /**********    Detected Correctness (testcase1)    **********/
                atomic_thread_fence(memory_order_acquire);
                if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
@@ -41,6 +45,9 @@ void seqlock::read(int *data1, int *data2) {
 void seqlock::write(int data1, int data2) {
        while (true) {
                // #1: either here or #2 must be acquire
+        // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to
+        // "memory_order_relaxed", run "make" to recompile, and then run:
+        // "./run.sh ./seqlock/testcase2 -m2 -y -u3 -x1000 -tSPEC"
                /**********    Detected Correctness (testcase2 with -y -x1000)    **********/
                int old_seq = _seq.load(memory_order_acquire); // acquire
                if (old_seq % 2 == 1) {
@@ -56,17 +63,24 @@ void seqlock::write(int data1, int data2) {
                }
        }
 
-       // XXX: Update the data. It needs to be release since this version use
+       // Update the data. It needs to be release since this version use
        // relaxed CAS in write(). When the first load of _seq reads the realaxed
        // CAS update, it does not form synchronization, thus requiring the data to
        // be acq/rel. The data in practice can be pointers to objects.
+
+    // XXX-injection-#4: Weaken the parameter "memory_order_release" to
+    // "memory_order_relaxed", run "make" to recompile, and then run:
+    // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
        /**********    Detected Correctness (testcase1)    **********/
        atomic_thread_fence(memory_order_release);
        _data1.store(data1, memory_order_relaxed);
        _data2.store(data2, memory_order_relaxed); 
        /** @OPDefine: true */
 
-       /**********    Detected Admissibility (testcase1)    **********/
+    // XXX-injection-#5: Weaken the parameter "memory_order_release" to
+    // "memory_order_relaxed", run "make" to recompile, and then run:
+    // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
+       /**********    Detected Correctness (testcase1)    **********/
        _seq.fetch_add(1, memory_order_release); // release
 }