From: Peizhao Ou <peizhaoo@uci.edu>
Date: Wed, 7 Dec 2016 23:23:27 +0000 (-0800)
Subject: add the comments for the mcs-lock and seqlock benchmarks that we changed during the... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d7cd5afd61141a6ce277bbcd192f132a3588e0f1;p=model-checker-benchmarks.git

add the comments for the mcs-lock and seqlock benchmarks that we changed during the artifact evaluation
---

diff --git a/mcs-lock/mcs-lock.cc b/mcs-lock/mcs-lock.cc
index 525ef9b..4ae59ff 100644
--- a/mcs-lock/mcs-lock.cc
+++ b/mcs-lock/mcs-lock.cc
@@ -77,6 +77,8 @@ void mcs_mutex::unlock(guard * I) {
         // "memory_order_relaxed", run "make" to recompile, and then run:
         // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC"
         /**********  Detected Correctness **********/
+        // This used the stronger mo_acq_rel parameter in old versions, but this
+        // is not necessary.
 		if ( m_tail.compare_exchange_strong(
 			tail_was_me,NULL,std::mo_release) ) {
 			// got null in tail, mutex is unlocked
diff --git a/seqlock/seqlock.cc b/seqlock/seqlock.cc
index ca4a55c..862dfd2 100644
--- a/seqlock/seqlock.cc
+++ b/seqlock/seqlock.cc
@@ -20,6 +20,8 @@ void seqlock::read(int *data1, int *data2) {
 		/**********    Detected Correctness (testcase1)    **********/
 		int old_seq = _seq.load(memory_order_acquire); // acquire
 		if (old_seq % 2 == 1) {
+            // The thrd_yield() operation is just for fairness but won't affect
+            // the correctness (and also the specification).
             thrd_yield();
             continue;
         }
@@ -35,6 +37,8 @@ void seqlock::read(int *data1, int *data2) {
 		/**********    Detected Correctness (testcase1)    **********/
 		atomic_thread_fence(memory_order_acquire);
 		if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
+            // The thrd_yield() operation is just for fairness but won't affect
+            // the correctness (and also the specification).
             thrd_yield();
 			return;
 		}
@@ -51,6 +55,8 @@ void seqlock::write(int data1, int data2) {
 		/**********    Detected Correctness (testcase2 with -y -x1000)    **********/
 		int old_seq = _seq.load(memory_order_acquire); // acquire
 		if (old_seq % 2 == 1) {
+            // The thrd_yield() operation is just for fairness but won't affect
+            // the correctness (and also the specification).
             thrd_yield();
 			continue; // Retry
         }
@@ -58,6 +64,8 @@ void seqlock::write(int data1, int data2) {
 		// #2
 		if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
 			memory_order_relaxed, memory_order_relaxed)) {
+            // The thrd_yield() operation is just for fairness but won't affect
+            // the correctness (and also the specification).
             thrd_yield();
 			break;
 		}