Working on external operations

harmonylang · Mar 22, 2024 · 1564de3 · 1564de3
1 parent 6eb4387
commit 1564de3
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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