From 722ae18e70d2658c04b7a7e53df2ab957aaab674 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 1 Oct 2012 13:20:56 -0700 Subject: [PATCH] action: synchronize_with - return status for out-of-order synchronization "synchronize_with()" now can return a boolean status, rather than just using an ASSERT(). This allows synchronize_with() to be called with actions that are against the program trace order, then return a status to signify success/failure. This will allow, for instance, release sequence calculations to simply abort this single execution, not the whole model-checker. --- action.cc | 7 +++++-- action.h | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/action.cc b/action.cc index 3fda30d..54ecce7 100644 --- a/action.cc +++ b/action.cc @@ -236,11 +236,14 @@ void ModelAction::read_from(const ModelAction *act) * Synchronize the current thread with the thread corresponding to the * ModelAction parameter. * @param act The ModelAction to synchronize with + * @return True if this is a valid synchronization; false otherwise */ -void ModelAction::synchronize_with(const ModelAction *act) { - ASSERT(*act < *this || type == THREAD_JOIN || type == ATOMIC_LOCK ); +bool ModelAction::synchronize_with(const ModelAction *act) { + if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK) + return false; model->check_promises(cv, act->cv); cv->merge(act->cv); + return true; } bool ModelAction::has_synchronized_with(const ModelAction *act) const diff --git a/action.h b/action.h index c455ea7..fecef4d 100644 --- a/action.h +++ b/action.h @@ -103,7 +103,7 @@ public: void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } void read_from(const ModelAction *act); - void synchronize_with(const ModelAction *act); + bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const; bool happens_before(const ModelAction *act) const; -- 2.34.1