From 3a6e0eecb8fd3cf626bd2aa8e62f1d6228b1f331 Mon Sep 17 00:00:00 2001 From: Robbert van Renesse Date: Sat, 19 Aug 2023 21:50:36 -0400 Subject: [PATCH 1/3] Added comments --- harmony_model_checker/charm/graph.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/harmony_model_checker/charm/graph.h b/harmony_model_checker/charm/graph.h index f72a343f..c446650b 100644 --- a/harmony_model_checker/charm/graph.h +++ b/harmony_model_checker/charm/graph.h @@ -44,6 +44,11 @@ struct access_info { // but, for memory efficiency, not the details of the microsteps themselves. If // a failure is found, that information is recovered by re-executing the path to // the faulty state. +// +// TODO. Can replace ctx with ctx_index into src->state, but should also +// support, say, -1 for inv_context. after could be replaced with +// an index into dst->state. choice could be the first entry in log +// Doing all three could save around 20 bytes per edge. struct edge { struct edge *fwdnext; // forward linked list maintenance hvalue_t ctx, choice; // ctx that made the microstep, choice if any From 90b632387132e543492a7f52f89ae3225c2562fe Mon Sep 17 00:00:00 2001 From: Robbert van Renesse Date: Tue, 22 Aug 2023 10:07:45 -0400 Subject: [PATCH 2/3] Using ./harmony instead of harmony in runall.scr --- runall.scr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/runall.scr b/runall.scr index bb0c309b..83b51230 100755 --- a/runall.scr +++ b/runall.scr @@ -1,4 +1,4 @@ -HARMONY=harmony +HARMONY=./harmony echo ============== echo triangle From 395fb4358a334f187c05cb466b2fcb32b28d3177 Mon Sep 17 00:00:00 2001 From: Robbert Van Renesse Date: Tue, 22 Aug 2023 12:00:09 -0400 Subject: [PATCH 3/3] Fixed bug --- harmony_model_checker/charm/ops.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c index f028d08d..704eb394 100644 --- a/harmony_model_checker/charm/ops.c +++ b/harmony_model_checker/charm/ops.c @@ -1374,6 +1374,7 @@ void op_Go( struct context *copy = (struct context *) buffer; ctx_push(copy, result); copy->stopped = false; + // TODO. Check success of context_add context_add(state, value_put_context(&step->engine, copy)); #ifdef HEAP_ALLOC free(buffer); @@ -2136,7 +2137,7 @@ void op_Spawn( } else { hvalue_t context = value_put_context(&step->engine, ctx); - if (!context_add(state, context)) { + if (context_add(state, context) < 0) { value_ctx_failure(step->ctx, &step->engine, "spawn: too many threads"); return; }