Returned most to the master branch

harmony_model_checker/charm/charm.h

@@ -99,6 +99,8 @@ struct global {
  unsigned int last_nstates; // to measure #states / second
  struct dfa *dfa; // for tracking correct behaviors
  unsigned int diameter; // graph diameter
+ bool phase2; // when model checking is done and graph analysis starts
+ struct scc *scc_todo; // SCC search
  struct json_value *pretty; // for output
  bool run_direct; // non-model-checked mode
  unsigned long allocated; // allocated table space

harmony_model_checker/charm/code.c

@@ -27,7 +27,6 @@ static struct instr code_instr_parse(struct engine *engine, struct json_value *j
  i.load = strcmp(oi->name, "Load") == 0;
  i.store = strcmp(oi->name, "Store") == 0;
  i.del = strcmp(oi->name, "Del") == 0;
- i.pause = strcmp(oi->name, "Pause") == 0;
  i.print = strcmp(oi->name, "Print") == 0;
  i.retop = strcmp(oi->name, "Return") == 0;
  i.atomicinc = strcmp(oi->name, "AtomicInc") == 0;

harmony_model_checker/charm/code.h

@@ -15,13 +15,12 @@ struct instr {
  // store: a Store instruction
  // del: a Del instruction
  // retop: a Return instruction
- // pause: a Pause instruction
  // print: a Print instruction
  // atomicinc: an AtomicInc instruction
  // atomicdec: an AtomicDec instruction
  // setintlevel: a SetIntlevel instruction
  // breakable: a Load, Store, Del, or AtomicInc instruction
- bool choose, load, store, del, retop, print, pause;
+ bool choose, load, store, del, retop, print;
  bool atomicinc, atomicdec, setintlevel, breakable;
 };
 

harmony_model_checker/charm/graph.c

@@ -74,16 +74,14 @@ void graph_check_for_data_race(
  struct node *node,
  struct engine *engine
 ) {
- struct state *state = node_state(node);
-
  // First check whether any edges conflict with themselves. That could
  // happen if more than one thread is in the same state and (all) write
  // the same variable
  for (struct edge *edge = node->fwd; edge != NULL; edge = edge->fwdnext) {
  for (struct access_info *ai = edge->ai; ai != NULL; ai = ai->next) {
  if (ai->indices != NULL) {
  assert(ai->n > 0);
- if (multiplicities(state)[edge->ctx_index] > 1 && !ai->load && !ai->atomic) {
+ if (edge->multiplicity > 1 && !ai->load && !ai->atomic) {
  struct failure *f = new_alloc(struct failure);
  f->type = FAIL_RACE;
  f->edge = node->u.ph2.u.to_parent;

harmony_model_checker/charm/graph.h

@@ -44,21 +44,18 @@ 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: various space saving options by replacing contexts with indices. Also
-// inv could be an invariant identifier rather than its pc.
 struct edge {
  struct edge *fwdnext; // forward linked list maintenance
- hvalue_t choice;  // choice if any (TODO, put in log[0] to save space)
+ hvalue_t ctx, choice; // ctx that made the microstep, choice if any
  struct node *src; // source node
  struct node *dst; // destination node
- hvalue_t after; // resulting context (TODO. index in dst context bag)
+ hvalue_t after; // resulting context
  struct access_info *ai; // to detect data races
- int16_t inv; // pc of invariant (negative if finally clause)
  uint16_t nsteps; // # microsteps
- uint8_t ctx_index;  // index of context in src state context bag
+ uint16_t multiplicity; // multiplicity of context
  bool interrupt : 1; // set if state change is an interrupt
  // TODO. Is choosing == (choice != 0)?
+ // Also, edge->src->choosing is probably the same
  bool choosing : 1; // destination state is choosing
  bool failed : 1; // context failed
  uint16_t nlog : 12; // size of print history

harmony_model_checker/charm/ops.c

@@ -729,11 +729,6 @@ void op_Continue(const void *env, struct state *state, struct step *step, struct
  step->ctx->pc++;
 }
 
-// TODO. Make the same as Continue?
-void op_Pause(const void *env, struct state *state, struct step *step, struct global *global){
- step->ctx->pc++;
-}
-
 // This is helper fumction to execute the return of a method call. Usually
 // this would be when a Return instruction is executed, but Charm also
 // supports built-in methods that need to return the same way. We also
@@ -1379,10 +1374,7 @@ void op_Go(
  struct context *copy = (struct context *) buffer;
  ctx_push(copy, result);
  copy->stopped = false;
- if (context_add(state, value_put_context(&step->engine, copy)) < 0) {
- value_ctx_failure(step->ctx, &step->engine, "Go: too many threads");
- return;
- }
+ context_add(state, value_put_context(&step->engine, copy));
 #ifdef HEAP_ALLOC
  free(buffer);
 #endif
@@ -2144,7 +2136,7 @@ void op_Spawn(
  }
  else {
  hvalue_t context = value_put_context(&step->engine, ctx);
- if (context_add(state, context) < 0) {
+ if (!context_add(state, context)) {
  value_ctx_failure(step->ctx, &step->engine, "spawn: too many threads");
  return;
  }
@@ -2560,7 +2552,6 @@ void *init_Choose(struct dict *map, struct engine *engine){ return NULL; }
 void *init_Continue(struct dict *map, struct engine *engine){ return NULL; }
 void *init_Dup(struct dict *map, struct engine *engine){ return NULL; }
 void *init_Go(struct dict *map, struct engine *engine){ return NULL; }
-void *init_Pause(struct dict *map, struct engine *engine){ return NULL; }
 void *init_Print(struct dict *map, struct engine *engine){ return NULL; }
 void *init_Pop(struct dict *map, struct engine *engine){ return NULL; }
 void *init_ReadonlyDec(struct dict *map, struct engine *engine){ return NULL; }
@@ -4458,7 +4449,6 @@ struct op_info op_table[] = {
  { "Nary", init_Nary, op_Nary },
  { "Pop", init_Pop, op_Pop },
  { "Print", init_Print, op_Print, next_Print },
- { "Pause", init_Pause, op_Pause },
  { "Push", init_Push, op_Push },
  { "ReadonlyDec", init_ReadonlyDec, op_ReadonlyDec },
  { "ReadonlyInc", init_ReadonlyInc, op_ReadonlyInc },

harmony_model_checker/charm/value.c

@@ -1608,7 +1608,7 @@ hvalue_t value_bag_add(struct engine *engine, hvalue_t bag, hvalue_t v, int mult
  return value_dict_store(engine, bag, v, count);
  }
  else {
- return value_dict_store(engine, bag, v, VALUE_TO_INT(multiplicity));
+ return value_dict_store(engine, bag, v, VALUE_TO_INT(1));
  }
 }
 
@@ -1741,39 +1741,33 @@ void context_remove(struct state *state, hvalue_t ctx){
  }
  else {
  state->bagsize--;
- memmove(
- &state_contexts(state)[i],
- &state_contexts(state)[i+1],
- (state->bagsize - i) * sizeof(hvalue_t) + i);
- memmove(
- (char *) &state_contexts(state)[state->bagsize] + i,
- (char *) &state_contexts(state)[state->bagsize + 1] + i + 1,
- state->bagsize - i);
+ memmove(&state_contexts(state)[i], &state_contexts(state)[i+1],
+ (state->bagsize - i) * sizeof(hvalue_t) + i);
+ memmove((char *) &state_contexts(state)[state->bagsize] + i,
+ (char *) &state_contexts(state)[state->bagsize + 1] + i + 1,
+ state->bagsize - i);
  }
- return;
+ break;
  }
  }
- printf("--> %p\n", (void *) ctx);
- panic("context_remove: no such context");
 }
 
-// Add context 'ctx' to the state's context bag. Return the index into the
-// context bag. Return -1 if there are too many different contexts
-// (i.e., >= MAX_CONTEXT_BAG).
-int context_add(struct state *state, hvalue_t ctx){
- int i;
+// Add context 'ctx' to the state's context bag. May fail if there are too
+// many different contexts (i.e., >= MAX_CONTEXT_BAG).
+bool context_add(struct state *state, hvalue_t ctx){
+ unsigned int i;
  for (i = 0; i < state->bagsize; i++) {
  if (state_contexts(state)[i] == ctx) {
  multiplicities(state)[i]++;
- return i;
+ return true;
  }
  if (state_contexts(state)[i] > ctx) {
  break;
  }
  }
 
  if (state->bagsize >= MAX_CONTEXT_BAG) {
- return -1;
+ return false;
  }
 
  // Move the last multiplicities
@@ -1788,5 +1782,5 @@ int context_add(struct state *state, hvalue_t ctx){
  state->bagsize++;
  state_contexts(state)[i] = ctx;
  multiplicities(state)[i] = 1;
- return i;
+ return true;
 }

harmony_model_checker/charm/value.h

@@ -7,25 +7,26 @@
 #include "charm.h"
 
 #define MAX_CONTEXT_STACK 250 // maximum size of context stack
-#define MAX_CONTEXT_BAG 32 // maximum number of distinct contexts
+#define MAX_CONTEXT_BAG  32 // maximum number of distinct contexts
 
 // This contains the state in a Harmony execution.
 //
 // TODO. State can be reduced in size in various ways;
 // - pre and stopbag are not always used
+// - choosing could be an index into the context bag
 // - the entire thing could be replaced with a collision-resistant hash
 typedef struct state {
  hvalue_t vars; // shared variables
  hvalue_t pre; // "pre" state (same as vars in non-choosing states)
+ hvalue_t choosing; // context that is choosing if non-zero
  hvalue_t stopbag; // bag of stopped contexts (to detect deadlock)
  uint32_t dfa_state; // state of input dfa
  uint16_t tid_gen; // thread id generator
- int8_t chooser; // -1 if not a choosing state, otherwise indexes into contexts
 
  // The state includes a variable-size bag of contexts. This is represented
  // by an array of contexts of type hvalue_t, which is followed by an array
  // of multiplicities (of type uint8_t) with the same number of elements.
- uint8_t bagsize;
+ uint16_t bagsize;
  // hvalue_t contexts[VAR_SIZE]; // context/multiplicity pairs
 } state;
 #define state_contexts(s) ((hvalue_t *) ((s) + 1))
@@ -141,9 +142,8 @@ void value_ctx_extend(struct context *ctx);
 hvalue_t value_ctx_failure(struct context *ctx, struct engine *engine, char *fmt, ...);
 bool value_ctx_all_eternal(hvalue_t ctxbag);
 bool value_state_all_eternal(struct state *state);
-void context_remove_by_index(struct state *state, int ctx_index);
 void context_remove(struct state *state, hvalue_t ctx);
-int context_add(struct state *state, hvalue_t ctx);
+bool context_add(struct state *state, hvalue_t ctx);
 char *json_escape_value(hvalue_t v);
 void value_trace(struct global *global, FILE *file, struct callstack *cs, unsigned int pc, hvalue_t vars, char *prefix);
 void print_vars(struct global *global, FILE *file, hvalue_t v);

harmony_model_checker/compile.py

@@ -5,8 +5,8 @@
 
 import harmony_model_checker.harmony.harmony as legacy_harmony
 from harmony_model_checker.harmony.harmony import Scope, Code, State
-from harmony_model_checker.harmony.ops import FrameOp, ReturnOp, PauseOp, JumpOp
-from harmony_model_checker.harmony.value import AddressValue, ContextValue, LabelValue
+from harmony_model_checker.harmony.ops import FrameOp, ReturnOp
+from harmony_model_checker.harmony.value import AddressValue, ContextValue
 from harmony_model_checker.parser.antlr_rule_visitor import HarmonyVisitorImpl
 from harmony_model_checker.parser.HarmonyParser import HarmonyParser
 from harmony_model_checker.parser.HarmonyErrorListener import HarmonyLexerErrorListener, HarmonyParserErrorListener
@@ -117,10 +117,6 @@ def _load_file(filename: str, scope: Scope, code: Code, init: bool):
  ast.compile(scope, code, None)
  if init:
  _, file, line, column = ast.token
- invlabel = LabelValue(None, "invariant")
- code.nextLabel(invlabel)
- code.append(PauseOp(), ast.token, ast.endtoken, stmt=(line1, column1, line2, column2))
- code.append(JumpOp(invlabel, reason="check invariants again"), ast.token, ast.token, stmt=(line1, column1, line2, column2))
  code.append(ReturnOp(("result", file, line, column), AddressValue(None, [])), ast.token, ast.endtoken, stmt=(line1, column1, line2, column2)) # to terminate "__init__" process
  legacy_harmony.namestack.pop()
 

harmony_model_checker/harmony/ops.py

@@ -668,23 +668,6 @@ def tladump(self):
  def eval(self, state, context):
  context.pc += 1
 
-# TODO. Maybe can be the same as ContinueOp
-class PauseOp(Op):
- def __repr__(self):
- return "Pause"
-
- def explain(self):
- return "yield to another thread"
-
- def jdump(self):
- return '{ "op": "Pause" }'
-
- def tladump(self):
- return 'OpPause(self)'
-
- def eval(self, state, context):
- context.pc += 1
-
 class StoreVarOp(Op):
  def __init__(self, v, lvar=None, reason=None):
  self.v = v
@@ -968,7 +951,7 @@ def __repr__(self):
  (lexeme, file, line, column) = self.result
  if self.default is None:
  return "ReturnOp(%s)"%lexeme
- return "ReturnOp(%s, %s)"%(lexeme, strValue(self.default))
+ return "ReturnOp(%s. %s)"%(lexeme, strValue(self.default))
 
  def jdump(self):
  if self.result is None: