Updated some things

Author: Robbert van Renesse

code/DinersCV2.hny

@@ -4,7 +4,7 @@ const N = 5
 
 mutex = synch.Lock()
 forks = [False,] * N
-conds = [synch.Condition(?mutex),] * N
+conds = [synch.Condition(),] * N
 
 def diner(which):
     let left, right = (which, (which + 1) % N):

code/atm.hny

@@ -16,12 +16,14 @@ def atm_check_balance(acct):    # return the balance on acct
     release(?accounts[acct].lock)
 
 def atm_withdraw(acct, amount): # withdraw amount from acct
+    assert amount >= 0
     acquire(?accounts[acct].lock)
     accounts[acct].balance -= amount
     result = True              # return success
     release(?accounts[acct].lock)
 
 def customer(atm, acct, amount):
+    assert amount >= 0
     let bal = atm_check_balance(acct):
         if amount <= bal:
             atm_withdraw(acct, amount)

code/linkedlist.hny

@@ -2,7 +2,7 @@ from synch import Lock, acquire, release
 from alloc import malloc, free
 
 def _node(v, n):     # allocate and initialize a new list node
-    result = malloc({ .lock: Lock(), .value: (0, v), .next: n })
+    result = malloc({ .lock: Lock(), .value: v, .next: n })
 
 def _find(lst, v):
     var before = lst
@@ -22,7 +22,7 @@ def SetObject():
 def insert(lst, v):
     let before, after = _find(lst, v):
         if after->value != (0, v):
-            before->next = _node(v, after)
+            before->next = _node((0, v), after)
         release(?after->lock)
         release(?before->lock)
 

code/lockspec.hny

@@ -6,5 +6,6 @@ def acquire(lk):
         !lk = True
 
 def release(lk):
-    assert !lk
-    atomically !lk = False
+    atomically:
+        assert !lk
+        !lk = False

code/locksusp.hny

@@ -6,7 +6,7 @@ def Lock():
 def acquire(lk):
     atomically:
         if lk->acquired:
-            stop lk->suspended[len lk->suspended]
+            stop ?lk->suspended[len lk->suspended]
             assert lk->acquired
         else:
             lk->acquired = True

code/queueMS.hny

@@ -1,4 +1,4 @@
-from synch import Lock, acquire, release
+from synch import Lock, acquire, release, atomic_load, atomic_store
 from alloc import malloc, free
 
 def Queue():
@@ -8,14 +8,14 @@ def Queue():
 def put(q, v):
     let node = malloc({ .value: v, .next: None }):
         acquire(?q->tllock)
-        q->tail->next = node
+        atomic_store(?q->tail->next,  node)
         q->tail = node
         release(?q->tllock)
 
 def get(q):
     acquire(?q->hdlock)
     let dummy = q->head
-    let node = dummy->next:
+    let node = atomic_load(?dummy->next):
         if node == None:
             result = None
             release(?q->hdlock)

code/queueconc.hny

@@ -2,7 +2,7 @@ from synch import Lock, acquire, release
 from alloc import malloc, free
 
 def Queue():
-    result = { .head: None, .tail: None, .lock: Lock(), .time: 0 }
+    result = { .head: None, .tail: None, .lock: Lock() }
 
 def put(q, v):
     let node = malloc({ .value: v, .next: None }):

code/ticket.hny

@@ -5,13 +5,16 @@ def fetch_and_increment(p):
         result = !p
         !p = (!p + 1) % MAX_THREADS
 
+def atomic_load(p):
+    atomically result = !p
+
 def Lock():
     result = { .counter: 0, .dispenser: 0 }
 
 def acquire(lk):
     let my_ticket = fetch_and_increment(?lk->dispenser):
-        atomically await lk->counter == my_ticket
+        while atomic_load(?lk->counter) != my_ticket:
+            pass
 
 def release(lk):
-    let next = (lk->counter + 1) % MAX_THREADS:
-        atomically lk->counter = next
+    fetch_and_increment(?lk->counter)

code/trap6.hny

@@ -1,10 +1,10 @@
 from synch import Lock, acquire, release
 
-sequential done
+sequential t_done, i_done
 
 count = 0
 countlock = Lock()
-done = [ False, False ]
+t_done = i_done = [ False, False ]
 
 def increment():
     let prior = setintlevel(True):
@@ -15,13 +15,15 @@ def increment():
 
 def handler(self):
     increment()
-    done[self] = True
+    i_done[self] = True
 
 def thread(self):
     trap handler(self)
     increment()
-    await all(done)
-    assert count == 4, count
+    await i_done[self]
+    t_done[self] = True
+    await all(t_done)
+    assert count == 4
 
 spawn thread(0)
 spawn thread(1)

harmony_model_checker/charm/charm.c

@@ -475,14 +475,15 @@ static bool onestep(
     }
 
     // Weight of this step
-    int weight = (node->to_parent == NULL || ctx == node->to_parent->after) ? 0 : 1;
+    unsigned int weight = (node->to_parent == NULL || ctx == node->to_parent->after) ? 0 : 1;
 
     // Allocate edge now
     struct edge *edge = walloc(w, sizeof(struct edge) + step->nlog * sizeof(hvalue_t), false);
     edge->src = node;
     edge->ctx = ctx;
     edge->choice = choice_copy;
     edge->interrupt = interrupt;
+    edge->weight = weight;
     edge->after = after;
     edge->ai = step->ai;
     memcpy(edge->log, step->log, step->nlog * sizeof(hvalue_t));
@@ -507,7 +508,9 @@ static bool onestep(
     else {
         unsigned int len = node->len + weight;
         unsigned int steps = node->steps + instrcnt;
-        if (len < next->len || (len == next->len && steps < next->steps)) {
+        // TODO: not sure how to minimize.  For some cases, this works better than
+        //   if (len < next->len || (len == next->len && steps < next->steps)) {
+        if (len < next->len || (len == next->len && steps <= next->steps)) {
             next->len = len;
             next->steps = steps;
             next->to_parent = edge;
@@ -2164,6 +2167,15 @@ int main(int argc, char **argv){
 
     printf("Phase 3: analysis\n");
     if (minheap_empty(global->failures)) {
+        double now = gettime();
+        global->phase2 = true;
+        global->scc_todo = scc_alloc(0, global->graph.size, NULL, NULL);
+        barrier_wait(&middle_barrier);
+        // Workers working on finding SCCs
+        barrier_wait(&end_barrier);
+
+        printf("%u components (%.3lf seconds)\n", global->ncomponents, gettime() - now);
+
 #ifdef DUMP_GRAPH
         printf("digraph Harmony {\n");
         for (unsigned int i = 0; i < global->graph.size; i++) {
@@ -2179,15 +2191,6 @@ int main(int argc, char **argv){
         printf("}\n");
 #endif
 
-        double now = gettime();
-        global->phase2 = true;
-        global->scc_todo = scc_alloc(0, global->graph.size, NULL, NULL);
-        barrier_wait(&middle_barrier);
-        // Workers working on finding SCCs
-        barrier_wait(&end_barrier);
-
-        printf("%u components (%.3lf seconds)\n", global->ncomponents, gettime() - now);
-
         // mark the components that are "good" because they have a way out
         struct component *components = calloc(global->ncomponents, sizeof(*components));
         for (unsigned int i = 0; i < global->graph.size; i++) {
@@ -2276,6 +2279,37 @@ int main(int argc, char **argv){
         }
     }
 
+#ifdef DUMP_GRAPH
+    if (true) {
+        FILE *df = fopen("charm.gv", "w");
+        fprintf(df, "digraph Harmony {\n");
+        for (unsigned int i = 0; i < global->graph.size; i++) {
+            struct node *node = global->graph.nodes[i];
+            fprintf(df, " s%u [label=\"%u/%u\"]\n", i, i, node->len);
+        }
+        for (unsigned int i = 0; i < global->graph.size; i++) {
+            struct node *node = global->graph.nodes[i];
+            for (struct edge *edge = node->fwd; edge != NULL; edge = edge->fwdnext) {
+                struct state *state = node->state;
+                unsigned int j;
+                for (j = 0; j < state->bagsize; j++) {
+                    if (state->contexts[j] == edge->ctx) {
+                        break;
+                    }
+                }
+                assert(j < state->bagsize);
+                fprintf(df, " s%u -> s%u [style=%s label=\"%u/%u\"]\n",
+                        node->id, edge->dst->id,
+                        edge->dst->to_parent == edge ? "solid" : "dashed",
+                        multiplicities(state)[j],
+                        edge->weight);
+            }
+        }
+        fprintf(df, "}\n");
+        fclose(df);
+    }
+#endif
+
 #ifdef OBSOLETE
     if (true) {
         FILE *df = fopen("charm.dump", "w");

harmony_model_checker/charm/graph.h

@@ -34,7 +34,8 @@ struct edge {
     struct access_info *ai;  // to detect data races
     uint16_t nsteps;         // # microsteps
     bool interrupt : 1;      // set if state change is an interrupt
-    uint16_t nlog : 15;      // size of print history
+    uint8_t weight : 1;      // context switch or not
+    uint16_t nlog : 14;      // size of print history
     hvalue_t log[0];         // print history (immediately follows edge)
 };
 

harmony_model_checker/harmony/verbose.py

@@ -122,6 +122,7 @@ def print_macrostep(self, f, mas):
                 print("shared variables:", file=f)
                 for k, v in self.shared.items():
                     print("  %s: %s"%(k, verbose_string(v)), file=f)
+            print("state id: %s"%mas["id"], file=f)
             print("================================================", file=f)
             self.lastmis = mis[0]
             self.start = int(self.lastmis["pc"])