Basic non-determinism checking for SC/TSO/PSO.

Will detect and report if a branch condition evaluates differently
during a replay of a computation.

doc/manual.tex

@@ -55,6 +55,11 @@ \section{Stateless Model Checking with DPOR}
 %
   This means that the test case may not e.g.\ check the time, or
   perform file I/O.
+%
+  If this condition is not satisfied, Nidhugg \emph{may} be able to
+  detect the nondeterminism and report it as an error with an attached
+  error trace (currently only supported under SC/TSO/PSO). However,
+  there is no guarantee for this, and a crash is a likely outcome.
 \end{description}
 
 \section{Supported Memory Models}

src/DetCheckTraceBuilder.cpp

@@ -0,0 +1,49 @@
+/* Copyright (C) 2017 Carl Leonardsson
+ *
+ * This file is part of Nidhugg.
+ *
+ * Nidhugg is free software: you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Nidhugg is distributed in the hope that it will be useful, but
+ * WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see
+ * <http://www.gnu.org/licenses/>.
+ */
+
+#include "DetCheckTraceBuilder.h"
+
+DetCheckTraceBuilder::DetCheckTraceBuilder(const Configuration &conf) : TraceBuilder(conf){
+  reset_cond_branch_log();
+}
+
+void DetCheckTraceBuilder::reset_cond_branch_log(){
+  cond_branch_log_index = 0;
+}
+
+bool DetCheckTraceBuilder::cond_branch(bool cnd){
+  if(is_replaying()){
+    assert(cond_branch_log_index < cond_branch_log.size());
+    bool logged = cond_branch_log[cond_branch_log_index];
+    ++cond_branch_log_index;
+    if(logged != cnd){
+      nondeterminism_error("Branch condition value changed in replay.");
+      return false;
+    }
+  }else{
+    if(cond_branch_log_index < cond_branch_log.size()){
+      cond_branch_log[cond_branch_log_index] = cnd;
+    }else{
+      assert(cond_branch_log_index == cond_branch_log.size());
+      cond_branch_log.push_back(cnd);
+    }
+    ++cond_branch_log_index;
+  }
+  return true;
+}

src/DetCheckTraceBuilder.h

@@ -0,0 +1,65 @@
+/* Copyright (C) 2017 Carl Leonardsson
+ *
+ * This file is part of Nidhugg.
+ *
+ * Nidhugg is free software: you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Nidhugg is distributed in the hope that it will be useful, but
+ * WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see
+ * <http://www.gnu.org/licenses/>.
+ */
+
+#include <config.h>
+
+#ifndef __DET_CHECK_TRACE_BUILDER_H__
+#define __DET_CHECK_TRACE_BUILDER_H__
+
+#include "TraceBuilder.h"
+
+/* A DetCheckTraceBuilder is an abstract TraceBuilder which adds some
+ * functionality for detecting and reporting thread-wise
+ * nondeterminism in the target program during computation replays.
+ */
+class DetCheckTraceBuilder : public TraceBuilder {
+public:
+  DetCheckTraceBuilder(const Configuration &conf = Configuration::default_conf);
+  virtual ~DetCheckTraceBuilder(){};
+  /* Execute a conditional branch instruction, branching on the value
+   * cnd.
+   *
+   * If thread-wise non-determinism is detected, an error is
+   * registered and false is returned. Otherwise true is returned.
+   */
+  virtual bool cond_branch(bool cnd);
+  /* Returns true if the currently scheduled event is a replay of a
+   * previous computation.
+   */
+  virtual bool is_replaying() const = 0;
+protected:
+  /* Call before starting a new computation to restart the branch
+   * logging.
+   */
+  virtual void reset_cond_branch_log();
+
+  /* cond_branch_log and cond_branch_log_index are used to log the
+   * conditional branches of a computation. cond_branch_log contains
+   * the branch condition values in order of execution. The first
+   * cond_branch_log_index entries in cond_branch_log correspond to
+   * branches that have been executed in the current
+   * computation. Later entries are carried over from previous
+   * (longer) computations. The carried-over entries are used to check
+   * that the branching is deterministic during computation replay.
+   */
+  std::vector<bool> cond_branch_log;
+  unsigned cond_branch_log_index; // See above
+};
+
+#endif

src/Execution.cpp

@@ -945,7 +945,12 @@ void Interpreter::visitBranchInst(BranchInst &I) {
   Dest = I.getSuccessor(0);          // Uncond branches have a fixed dest...
   if (!I.isUnconditional()) {
     Value *Cond = I.getCondition();
-    if (getOperandValue(Cond, SF).IntVal == 0) // If false cond...
+    bool condVal = (getOperandValue(Cond, SF).IntVal != 0);
+    if(!TB.cond_branch(condVal)){
+      abort();
+      return;
+    }
+    if (!condVal) // If false cond...
       Dest = I.getSuccessor(1);
   }
   SwitchToNewBasicBlock(Dest, SF);
@@ -3350,6 +3355,7 @@ void Interpreter::clearAllStacks(){
 }
 
 void Interpreter::abort(){
+  TB.cancel_replay();
   for(unsigned i = 0; i < Threads.size(); ++i){
     TB.mark_unavailable(i);
   }

src/Makefile.am

@@ -8,6 +8,7 @@ libnidhugg_a_SOURCES = \
   Configuration.cpp Configuration.h \
   CPid.cpp CPid.h \
   Debug.cpp Debug.h \
+  DetCheckTraceBuilder.cpp DetCheckTraceBuilder.h \
   DPORDriver.cpp DPORDriver.h \
   Execution.cpp \
   ExternalFunctions.cpp \

src/PSOTraceBuilder.cpp

@@ -208,6 +208,16 @@ void PSOTraceBuilder::mark_unavailable(int proc, int aux){
   mark_unavailable_ipid(ipid(proc,aux));
 }
 
+bool PSOTraceBuilder::is_replaying() const {
+  return replay;
+}
+
+void PSOTraceBuilder::cancel_replay(){
+  if(!replay) return;
+  replay = false;
+  prefix.resize(prefix_idx+1,Event(IID<IPid>(),VClock<IPid>()));
+}
+
 void PSOTraceBuilder::metadata(const llvm::MDNode *md){
   if(curnode().md == 0){
     curnode().md = md;
@@ -315,6 +325,7 @@ bool PSOTraceBuilder::reset(){
   available_auxs.clear();
   available_threads.insert(0);
   last_md = 0;
+  reset_cond_branch_log();
 
   return true;
 }

src/PSOTraceBuilder.h

@@ -32,6 +32,8 @@ class PSOTraceBuilder : public TSOPSOTraceBuilder{
   virtual void refuse_schedule();
   virtual void mark_available(int proc, int aux = -1);
   virtual void mark_unavailable(int proc, int aux = -1);
+  virtual void cancel_replay();
+  virtual bool is_replaying() const;
   virtual void metadata(const llvm::MDNode *md);
   virtual bool sleepset_is_empty() const;
   virtual bool check_for_cycles();

src/PSO_test2.cpp

@@ -1163,6 +1163,64 @@ declare void @__assert_fail() nounwind noreturn
   BOOST_CHECK(DPORDriver_test::check_all_traces(res,expected,conf));
 }
 
+BOOST_AUTO_TEST_CASE(Nondeterminism_detection){
+  /* Simulate thread-wise nondeterminism, and check that it is
+   * detected.
+   *
+   * Here we use a memory location _changing_ which is declared
+   * *outside* of the test code. This is in order to ensure that its
+   * value is not reinitialized when the test is restarted (as a
+   * static variable inside the test code would be).
+   *
+   * The code in main will run twice. (This is ensured by the race on
+   * x.)
+   *
+   * The code in main branches on the value of _changing_, and changes
+   * its value. Therefore the branch will go in different directions
+   * in the first and the second computation. Since the branch is
+   * evaluated in the portion of the code that is replayed, this
+   * apparent non-determinism should be detected and trigger an error.
+   */
+  Configuration conf = DPORDriver_test::get_pso_conf();
+  char changing = 0;
+  std::stringstream ss;
+  ss << "inttoptr(i64 " << (unsigned long)(&changing) << " to i8*)";
+  std::string changingAddr = ss.str();
+  DPORDriver *driver =
+    DPORDriver::parseIR(StrModule::portasm(R"(
+@x = global i32 0, align 4
+
+define i8* @p1(i8* %arg){
+  store i32 1, i32* @x
+  ret i8* null
+}
+
+define i32 @main(){
+  %v = load i8, i8* )"+changingAddr+R"(
+  %c = icmp eq i8 %v, 0
+  br i1 %c, label %doset, label %exit
+doset:
+  store i8 1, i8* )"+changingAddr+R"(
+  br label %exit
+exit:
+  call i32 @pthread_create(i64* null, %attr_t* null, i8*(i8*)* @p1, i8* null)
+  load i32, i32* @x
+  ret i32 0
+}
+
+%attr_t = type { i64, [48 x i8] }
+declare i32 @pthread_create(i64*, %attr_t*, i8*(i8*)*, i8*) nounwind
+declare void @__assert_fail()
+)"),conf);
+
+  DPORDriver::Result res = driver->run();
+
+  BOOST_CHECK(changing == 1);
+  BOOST_CHECK(res.has_errors());
+
+  delete driver;
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 #endif

src/SC_test2.cpp

@@ -327,6 +327,64 @@ declare i32 @pthread_create(i64*, %attr_t*, i8*(i8*)*, i8*) nounwind
   delete driver;
 }
 
+BOOST_AUTO_TEST_CASE(Nondeterminism_detection){
+  /* Simulate thread-wise nondeterminism, and check that it is
+   * detected.
+   *
+   * Here we use a memory location _changing_ which is declared
+   * *outside* of the test code. This is in order to ensure that its
+   * value is not reinitialized when the test is restarted (as a
+   * static variable inside the test code would be).
+   *
+   * The code in main will run twice. (This is ensured by the race on
+   * x.)
+   *
+   * The code in main branches on the value of _changing_, and changes
+   * its value. Therefore the branch will go in different directions
+   * in the first and the second computation. Since the branch is
+   * evaluated in the portion of the code that is replayed, this
+   * apparent non-determinism should be detected and trigger an error.
+   */
+  Configuration conf = DPORDriver_test::get_sc_conf();
+  char changing = 0;
+  std::stringstream ss;
+  ss << "inttoptr(i64 " << (unsigned long)(&changing) << " to i8*)";
+  std::string changingAddr = ss.str();
+  DPORDriver *driver =
+    DPORDriver::parseIR(StrModule::portasm(R"(
+@x = global i32 0, align 4
+
+define i8* @p1(i8* %arg){
+  store i32 1, i32* @x
+  ret i8* null
+}
+
+define i32 @main(){
+  %v = load i8, i8* )"+changingAddr+R"(
+  %c = icmp eq i8 %v, 0
+  br i1 %c, label %doset, label %exit
+doset:
+  store i8 1, i8* )"+changingAddr+R"(
+  br label %exit
+exit:
+  call i32 @pthread_create(i64* null, %attr_t* null, i8*(i8*)* @p1, i8* null)
+  load i32, i32* @x
+  ret i32 0
+}
+
+%attr_t = type { i64, [48 x i8] }
+declare i32 @pthread_create(i64*, %attr_t*, i8*(i8*)*, i8*) nounwind
+declare void @__assert_fail()
+)"),conf);
+
+  DPORDriver::Result res = driver->run();
+
+  BOOST_CHECK(changing == 1);
+  BOOST_CHECK(res.has_errors());
+
+  delete driver;
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 #endif

src/TSOPSOTraceBuilder.h

@@ -25,7 +25,7 @@
 #include "Configuration.h"
 #include "MRef.h"
 #include "Trace.h"
-#include "TraceBuilder.h"
+#include "DetCheckTraceBuilder.h"
 
 #include <string>
 #include <vector>
@@ -44,10 +44,10 @@
  * memory model specific.
  */
 
-class TSOPSOTraceBuilder : public TraceBuilder{
+class TSOPSOTraceBuilder : public DetCheckTraceBuilder{
 public:
   TSOPSOTraceBuilder(const Configuration &conf = Configuration::default_conf)
-    : TraceBuilder(conf) {};
+    : DetCheckTraceBuilder(conf) {};
   virtual ~TSOPSOTraceBuilder() {};
   /* Schedules the next thread.
    *
@@ -96,6 +96,11 @@ class TSOPSOTraceBuilder : public TraceBuilder{
    * because it is blocked waiting for something.
    */
   virtual void mark_unavailable(int proc, int aux = -1) = 0;
+  /* If we are not in a replay, do nothing. Otherwise cancel the
+   * replay from here on, so that the computation may continue
+   * according to an arbitrary schedule.
+   */
+  virtual void cancel_replay() = 0;
   /* Associate the currently scheduled event with LLVM "dbg" metadata. */
   virtual void metadata(const llvm::MDNode *md) = 0;
 

src/TSOTraceBuilder.cpp

@@ -160,6 +160,16 @@ void TSOTraceBuilder::mark_unavailable(int proc, int aux){
   threads[ipid(proc,aux)].available = false;
 }
 
+bool TSOTraceBuilder::is_replaying() const {
+  return replay;
+}
+
+void TSOTraceBuilder::cancel_replay(){
+  if(!replay) return;
+  replay = false;
+  prefix.resize(prefix_idx+1,Event(IID<IPid>(),VClock<IPid>()));
+}
+
 void TSOTraceBuilder::metadata(const llvm::MDNode *md){
   if(!dryrun && curnode().md == 0){
     curnode().md = md;
@@ -266,6 +276,7 @@ bool TSOTraceBuilder::reset(){
   replay = true;
   dry_sleepers = 0;
   last_md = 0;
+  reset_cond_branch_log();
 
   return true;
 }

src/TSOTraceBuilder.h

@@ -32,6 +32,8 @@ class TSOTraceBuilder : public TSOPSOTraceBuilder{
   virtual void refuse_schedule();
   virtual void mark_available(int proc, int aux = -1);
   virtual void mark_unavailable(int proc, int aux = -1);
+  virtual void cancel_replay();
+  virtual bool is_replaying() const;
   virtual void metadata(const llvm::MDNode *md);
   virtual bool sleepset_is_empty() const;
   virtual bool check_for_cycles();