From: Brian Norris <banorris@uci.edu>
Date: Wed, 13 Feb 2013 02:12:17 +0000 (-0800)
Subject: model: add 'pending' assertion
X-Git-Tag: oopsla2013~255
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=61eabdb86ab3a0a9a3051bd0bbf4dfed2172fdce;hp=8b2d7b35e955c675bbfd1f415d25b01494cc330f

model: add 'pending' assertion

We don't want to clobber a pending action.
---

diff --git a/model.cc b/model.cc
index 97f235c..01e4c49 100644
--- a/model.cc
+++ b/model.cc
@@ -2663,6 +2663,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
 	DBG();
 	Thread *old = thread_current();
+	ASSERT(!old->get_pending());
 	old->set_pending(act);
 	if (Thread::swap(old, &system_context) < 0) {
 		perror("swap threads");