diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c index 72f8e556..bfcfd6b1 100644 --- a/harmony_model_checker/charm/charm.c +++ b/harmony_model_checker/charm/charm.c @@ -302,7 +302,7 @@ static inline void context_remove_by_index(struct state *state, int i){ } // Part of experimental -d option, running Harmony programs "for real". -static void run_direct(struct state *state){ +static void direct_run(struct state *state){ struct { struct context ctx; hvalue_t stack[MAX_CONTEXT_STACK]; @@ -315,7 +315,12 @@ static void run_direct(struct state *state){ setbuf(stdout, NULL); - while (state->bagsize > 0) { + while (state->total > 0) { + direct_check(state, &step); + if (state->bagsize == 0) { + continue; + } + unsigned int total = 0, ctx_index = 0; for (int i = 0; i < state->bagsize; i++) { total += state_multiplicity(state, i); @@ -354,7 +359,7 @@ static void run_direct(struct state *state){ struct instr *instrs = global.code.instrs; struct op_info *oi = instrs[pc].oi; (*oi->op)(instrs[pc].env, state, &step); - if (step.ctx->terminated) { + if (step.ctx->terminated || step.ctx->stopped) { break; } if (step.ctx->failed) { @@ -410,7 +415,11 @@ static void run_direct(struct state *state){ context_remove_by_index(state, ctx_index); // Add updated context to state unless terminated or stopped - if (!step.ctx->terminated && !step.ctx->stopped) { + if (step.ctx->stopped) { + hvalue_t after = value_put_context(step.allocator, step.ctx); + stopped_context_add(state, after); + } + else if (!step.ctx->terminated) { hvalue_t after = value_put_context(step.allocator, step.ctx); context_add(state, after); } @@ -3787,7 +3796,7 @@ int exec_model_checker(int argc, char **argv){ if (dflag) { global.run_direct = true; srand((unsigned) gettime()); - run_direct(state); + direct_run(state); exit(0); } diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c index 1d593a98..05dbfbf2 100644 --- a/harmony_model_checker/charm/ops.c +++ b/harmony_model_checker/charm/ops.c @@ -960,7 +960,7 @@ static void direct_completed(hvalue_t ctx, hvalue_t result){ } // See if any external activities completed. -static void direct_check(struct state *state, struct step *step){ +void direct_check(struct state *state, struct step *step){ mutex_acquire(&direct_mutex); struct direct_done *dd; @@ -1006,7 +1006,7 @@ static void direct_check(struct state *state, struct step *step){ // Add new context to the context bag if (context_add(state, context) < 0) { - value_ctx_failure(step->ctx, step->allocator, "direct_check: too many threads"); + panic("direct_check: too many threads"); } free(dd); } @@ -1033,6 +1033,8 @@ void op_Bogus_Bogus(const void *env, struct state *state, struct step *step){ step->ctx->pc++; step->ctx->stopped = true; + printf("op_Bogus\n"); + // Save the context hvalue_t v = value_put_context(step->allocator, step->ctx); diff --git a/harmony_model_checker/charm/ops.h b/harmony_model_checker/charm/ops.h index 5b8a4917..bfcda094 100644 --- a/harmony_model_checker/charm/ops.h +++ b/harmony_model_checker/charm/ops.h @@ -154,5 +154,6 @@ struct env_StoreVar { }; void interrupt_invoke(struct step *step); +void direct_check(struct state *state, struct step *step); #endif //SRC_OPS_H