projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
threads/model: allocate Thread from w/in ModelChecker
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index ef9bed305fc0295af447e25365cccd6a8f2399a3..400adc208047f8d2c7b4700c31bc20b650854e34 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-48,6
+48,7
@@
struct model_snapshot_members {
stats(),
failed_promise(false),
too_many_reads(false),
stats(),
failed_promise(false),
too_many_reads(false),
+ no_valid_reads(false),
bad_synchronization(false),
asserted(false)
{ }
bad_synchronization(false),
asserted(false)
{ }
@@
-66,6
+67,7
@@
struct model_snapshot_members {
struct execution_stats stats;
bool failed_promise;
bool too_many_reads;
struct execution_stats stats;
bool failed_promise;
bool too_many_reads;
+ bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
bool asserted;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
bool asserted;
@@
-294,7
+296,6
@@
void ModelChecker::execute_sleep_set()
thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
- thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
priv->current_action->set_sleep_flag();
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
priv->current_action->set_sleep_flag();
@@
-968,7
+969,10
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
- Thread *th = curr->get_thread_operand();
+ thrd_t *thrd = (thrd_t *)curr->get_location();
+ struct thread_params *params = (struct thread_params *)curr->get_value();
+ Thread *th = new Thread(thrd, params->func, params->arg);
+ add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises->size(); i++) {
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises->size(); i++) {
@@
-1387,6
+1391,8
@@
void ModelChecker::print_infeasibility(const char *prefix) const
ptr += sprintf(ptr, "[failed promise]");
if (priv->too_many_reads)
ptr += sprintf(ptr, "[too many reads]");
ptr += sprintf(ptr, "[failed promise]");
if (priv->too_many_reads)
ptr += sprintf(ptr, "[too many reads]");
+ if (priv->no_valid_reads)
+ ptr += sprintf(ptr, "[no valid reads-from]");
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
if (promises_expired())
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
if (promises_expired())
@@
-1415,6
+1421,7
@@
bool ModelChecker::is_feasible_prefix_ignore_relseq() const
bool ModelChecker::is_infeasible() const
{
return mo_graph->checkForCycles() ||
bool ModelChecker::is_infeasible() const
{
return mo_graph->checkForCycles() ||
+ priv->no_valid_reads ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
@@
-1494,13
+1501,9
@@
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
continue;
/* Test to see whether this is a feasible write to read from */
continue;
/* Test to see whether this is a feasible write to read from */
- mo_graph->startChanges();
- r_modification_order(curr, write);
- bool feasiblereadfrom = !is_infeasible();
- mo_graph->rollbackChanges();
+ /** NOTE: all members of read-from set should be
+ * feasible, so we no longer check it here **/
- if (!feasiblereadfrom)
- continue;
rit = ritcopy;
bool feasiblewrite = true;
rit = ritcopy;
bool feasiblewrite = true;
@@
-2473,14
+2476,25
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
- if (allow_read)
- curr->get_node()->add_read_from(act);
+ if (allow_read) {
+ /* Only add feasible reads */
+ mo_graph->startChanges();
+ r_modification_order(curr, act);
+ if (!is_infeasible())
+ curr->get_node()->add_read_from(act);
+ mo_graph->rollbackChanges();
+ }
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
break;
}
}
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
break;
}
}
+ /* We may find no valid may-read-from only if the execution is doomed */
+ if (!curr->get_node()->get_read_from_size()) {
+ priv->no_valid_reads = true;
+ set_assert();
+ }
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
@@
-2665,7
+2679,6
@@
uint64_t ModelChecker::switch_to_master(ModelAction *act)
DBG();
Thread *old = thread_current();
set_current_action(act);
DBG();
Thread *old = thread_current();
set_current_action(act);
- old->set_state(THREAD_READY);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
@@
-2733,13
+2746,10
@@
bool ModelChecker::take_step(ModelAction *curr)
if (!next_thrd)
return false;
if (!next_thrd)
return false;
- next_thrd->set_state(THREAD_RUNNING);
-
if (next_thrd->get_pending() != NULL) {
/* restart a pending action */
set_current_action(next_thrd->get_pending());
next_thrd->set_pending(NULL);
if (next_thrd->get_pending() != NULL) {
/* restart a pending action */
set_current_action(next_thrd->get_pending());
next_thrd->set_pending(NULL);
- next_thrd->set_state(THREAD_READY);
return true;
}
return true;
}