From 1734b98c1384bed516df35d0d571f6a0037a7131 Mon Sep 17 00:00:00 2001 From: Robbert van Renesse Date: Tue, 22 Aug 2023 14:18:31 -0400 Subject: [PATCH] Found and fixed a bug --- harmony_model_checker/charm/charm.c | 35 ++++++++++++++++++++++++++--- harmony_model_checker/charm/ops.c | 18 ++++++++++++++- harmony_model_checker/charm/value.c | 4 +++- runall.py | 11 ++++----- 4 files changed, 58 insertions(+), 10 deletions(-) diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c index 1d41d327..a71dd5fa 100644 --- a/harmony_model_checker/charm/charm.c +++ b/harmony_model_checker/charm/charm.c @@ -1497,7 +1497,9 @@ void path_recompute(struct global *global){ pid = global->oldpid; } else { + // printf("Search for %p\n", (void *) ctx); for (pid = 0; pid < global->nprocesses; pid++) { + // printf("%d: %p\n", pid, (void *) global->processes[pid]); if (global->processes[pid] == ctx) { break; } @@ -1508,6 +1510,9 @@ void path_recompute(struct global *global){ printf("PID %p %u %u\n", (void *) ctx, pid, global->nprocesses); panic("bad pid"); } + else { + // printf("Found %d\n", pid); + } assert(pid < global->nprocesses); macro->tid = pid; @@ -1527,6 +1532,8 @@ void path_recompute(struct global *global){ ); assert(global->processes[pid] == e->after || e->after == 0); + // printf("Set %d to %p\n", pid, (void *) e->after); + // Copy thread state macro->nprocesses = global->nprocesses; macro->processes = copy(global->processes, global->nprocesses * sizeof(hvalue_t)); @@ -3701,6 +3708,8 @@ int exec_model_checker(int argc, char **argv){ printf("* Phase 3: analysis\n"); + bool computed_components = false; + // If no failures were detected (yet), determine strongly connected components // and look for non-terminating states. if (global->failures == NULL) { @@ -3710,6 +3719,7 @@ int exec_model_checker(int argc, char **argv){ } double now = gettime(); tarjan(global); + computed_components = true; // Compute shortest path to initial state for each node. shortest_path(global); @@ -3931,7 +3941,10 @@ int exec_model_checker(int argc, char **argv){ struct node *node = global->graph.nodes[i]; assert(node->id == i); fprintf(df, "\nNode %d:\n", node->id); - fprintf(df, " component: %d\n", node->u.ph2.component); + if (computed_components) { + fprintf(df, " component: %d\n", node->u.ph2.component); + } + fprintf(df, " len to parent: %d\n", node->u.ph2.len); if (node->u.ph2.u.to_parent != NULL) { fprintf(df, " ancestors:"); for (struct node *n = node->u.ph2.u.to_parent->src;; n = n->u.ph2.u.to_parent->src) { @@ -3942,7 +3955,21 @@ int exec_model_checker(int argc, char **argv){ } fprintf(df, "\n"); } - fprintf(df, " vars: %s\n", value_string(node_state(node)->vars)); + struct state *state = node_state(node); + fprintf(df, " vars: %s\n", value_string(state->vars)); + fprintf(df, " contexts:\n"); + for (unsigned int i = 0; i < state->bagsize; i++) { + fprintf(df, " %"PRI_HVAL": %u\n", state_contexts(state)[i], multiplicities(state)[i]); + } + if (state->stopbag != VALUE_DICT) { + fprintf(df, " stopbag:\n"); + unsigned int size; + hvalue_t *vals = value_get(state->stopbag, &size); + size /= 2 * sizeof(hvalue_t); + for (unsigned int i = 0; i < size; i++) { + fprintf(df, " %"PRI_HVAL": %d\n", vals[2*i], (int) VALUE_FROM_INT(vals[2*i+1]));; + } + } // fprintf(df, " len: %u %u\n", node->len, node->steps); if (node->failed) { fprintf(df, " failed\n"); @@ -4058,7 +4085,9 @@ int exec_model_checker(int argc, char **argv){ } fprintf(out, " {\n"); fprintf(out, " \"idx\": %d,\n", node->id); - fprintf(out, " \"component\": %d,\n", node->u.ph2.component); + if (computed_components) { + fprintf(out, " \"component\": %d,\n", node->u.ph2.component); + } #ifdef notdef if (node->parent != NULL) { fprintf(out, " \"parent\": %d,\n", node->parent->id); diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c index 704eb394..86cd1f04 100644 --- a/harmony_model_checker/charm/ops.c +++ b/harmony_model_checker/charm/ops.c @@ -1375,11 +1375,26 @@ void op_Go( ctx_push(copy, result); copy->stopped = false; // TODO. Check success of context_add - context_add(state, value_put_context(&step->engine, copy)); + hvalue_t context = value_put_context(&step->engine, copy); + context_add(state, context); #ifdef HEAP_ALLOC free(buffer); #endif step->ctx->pc++; + + if (step->keep_callstack) { + // Find the process + unsigned int pid; + for (pid = 0; pid < global->nprocesses; pid++) { + if (global->processes[pid] == ctx) { + global->processes[pid] = context; + break; + } + } + if (pid >= global->nprocesses) { + panic("op_Go: can't find process"); + } + } } void op_Finally(const void *env, struct state *state, struct step *step, struct global *global){ @@ -2147,6 +2162,7 @@ void op_Spawn( global->processes = realloc(global->processes, (global->nprocesses + 1) * sizeof(hvalue_t)); global->callstacks = realloc(global->callstacks, (global->nprocesses + 1) * sizeof(struct callstack *)); global->processes[global->nprocesses] = context; + // printf("Add %d %p\n", global->nprocesses, (void *) context); struct callstack *cs = new_alloc(struct callstack); cs->pc = pc; cs->arg = arg; diff --git a/harmony_model_checker/charm/value.c b/harmony_model_checker/charm/value.c index d9f7dcd2..add28689 100644 --- a/harmony_model_checker/charm/value.c +++ b/harmony_model_checker/charm/value.c @@ -1747,9 +1747,11 @@ void context_remove(struct state *state, hvalue_t ctx){ (char *) &state_contexts(state)[state->bagsize + 1] + i + 1, state->bagsize - i); } - break; + return; } } + // TODO. this can happen with invariant contexts + // panic("context_remove: can't find context"); } // Add context 'ctx' to the state's context bag. May fail if there are too diff --git a/runall.py b/runall.py index 7f78ca7a..a576f35a 100644 --- a/runall.py +++ b/runall.py @@ -17,7 +17,7 @@ { "args": "code/naiveTurn.hny", "issue": "Non-terminating state", "nstates": 28 }, { "args": "code/Peterson.hny", "issue": "No issues", "nstates": 104 }, { "args": "code/PetersonBroken.hny", "issue": "Safety violation", "nstates": 126 }, - { "args": "code/PetersonInductive.hny", "issue": "No Issues", "nstates": 4 }, + { "args": "code/PetersonInductive.hny", "issue": "No issues", "nstates": 104 }, { "args": "code/csonebit.hny", "issue": "Active busy waiting", "nstates": 73 }, { "args": "code/PetersonMethod.hny", "issue": "No issues", "nstates": 104 }, { "args": "code/hanoi.hny", "issue": "Safety violation", "nstates": 28 }, @@ -29,7 +29,7 @@ { "args": "-msynch=synchS code/UpLock.hny", "issue": "No issues", "nstates": 58 }, { "args": "code/spinlock.hny", "issue": "No issues", "nstates": 473 }, { "args": "code/xy.hny", "issue": "Safety violation", "nstates": 19 }, - { "args": "code/atm.hny", "issue": "Safety violation", "nstates": 128 }, + { "args": "code/atm.hny", "issue": "Invariant violation", "nstates": 1832 }, { "args": "code/queuedemo.hny", "issue": "No issues", "nstates": 80 }, { "args": "code/setobjtest.hny", "issue": "No issues", "nstates": 217 }, { "args": "-msetobj=linkedlist code/setobjtest.hny", "issue": "No issues", "nstates": 9495 }, @@ -44,7 +44,7 @@ { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 }, { "args": "-B queue4.hfa -m queue=queueconc code/qtestpar.hny", "issue": "No issues", "nstates": 66530 }, { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 }, - { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 }, + { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "No issues", "nstates": 99816 }, { "args": "-mqueue=queuebroken code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 }, { "args": "code/RWtest.hny", "issue": "No issues", "nstates": 135 }, { "args": "-mRW=RWsbs code/RWtest.hny", "issue": "No issues", "nstates": 1757 }, @@ -84,7 +84,7 @@ { "args": "-msynch=synchS code/trap6.hny", "issue": "No issues", "nstates": 554 }, { "args": "code/hw.hny", "issue": "No issues", "nstates": 23864 }, { "args": "code/abptest.hny", "issue": "No issues", "nstates": 2778 }, - { "args": "code/leader.hny", "issue": "Safety violation", "nstates": 117 }, + { "args": "code/leader.hny", "issue": "No issues", "nstates": 33005 }, { "args": "-mstack=stack1 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, { "args": "-mstack=stack2 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, { "args": "-mstack=stack3 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, @@ -106,8 +106,9 @@ if t["issue"] != hco["issue"]: print("Different issue (was %s)??? Aborting further tests" % t["issue"]) break - if min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9: + if t["issue"] != "Safety violation" and min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9: print("#states very different (was %d)??? Aborting further tests" % t["nstates"]) + break else: print("Error code %d, aborting further tests" % cp.returncode) print("Output: ", cp.stdout)