Merge branch 'next'

code/abd.hny

@@ -10,8 +10,8 @@ def send(m): atomically network = bag.add(network, m)
 def server():
     var t, v, received = (0, None), None, {}
     while True:
-        atomically when exists m in { m for m in keys network - received
-                            where m.type in {"read", "write"} }:
+        atomically when exists m in { k for k in keys network - received
+                            where k.type in {"read", "write"} }:
             received |= { m }
             if (m.type == "write") and (m.value[0] > t):
                 t, v = m.value

code/bqueueconc.hny

@@ -0,0 +1,110 @@
+import list
+from alloc import malloc, free
+
+def atomic_load(p):
+    atomically result = !p
+
+def atomic_store(p, v):
+    atomically !p = v
+
+def tas(lk):
+    atomically:
+        result = !lk
+        !lk = True
+
+def cas(p, old, new):
+    atomically:
+        result = !p == old
+        if result:
+            !p = new
+
+def BinSema(initial):
+    result = { .acquired: initial, .suspended: [] }
+
+def Lock():
+    result = BinSema(False)
+
+def acquire(binsema):
+    atomically:
+        if binsema->acquired:
+            stop ?binsema->suspended[len binsema->suspended]
+            assert binsema->acquired
+        else:
+            binsema->acquired = True
+
+def release(binsema):
+    atomically:
+        assert binsema->acquired
+        if binsema->suspended == []:
+            binsema->acquired = False
+        else:
+            go (binsema->suspended[0]) ()
+            del binsema->suspended[0]
+
+def held(binsema):
+    result = binsema->acquired
+
+def Condition():
+    result = []
+
+def wait(c, lk):
+    atomically:
+        release(lk)
+        stop ?(!c)[len !c]
+    acquire(lk)
+
+def notify(c):
+    atomically if !c != []:
+        go (list.head(!c)) ()
+        !c = list.tail(!c)
+
+def notifyAll(c):
+    atomically:
+        while !c != []:
+            go (list.head(!c)) ()
+            !c = list.tail(!c)
+
+def Semaphore(cnt):
+    result = { .count: cnt, .waiters: [] }
+
+def P(sema):
+    atomically:
+        if sema->count > 0:
+            sema->count -= 1
+        else:
+            stop ?sema->waiters[len sema->waiters]
+
+def V(sema):
+    atomically let cnt, waiters = sema->count, sema->waiters:
+        if waiters != []:
+            assert cnt == 0
+            go (waiters[0]) ()
+            sema->waiters = list.tail(waiters)
+        else:
+            sema->count = cnt + 1
+
+def Queue() returns empty:
+    empty = { .head: None, .tail: None, .lock: Lock(), .cv: Condition() }
+
+def put(q, v):
+    let node = malloc({ .value: v, .next: None }):
+        acquire(?q->lock)
+        if q->tail == None:
+            q->tail = q->head = node
+        else:
+            q->tail->next = node
+            q->tail = node
+        notify(?q->cv)
+        release(?q->lock)
+
+def get(q) returns next:
+    acquire(?q->lock)
+    while q->head == None:
+        wait(?q->cv, ?q->lock)
+    let node = q->head:
+        next = node->value
+        q->head = node->next
+        if q->head == None:
+            q->tail = None
+        free(node)
+    release(?q->lock)

code/fs.hny

@@ -24,7 +24,7 @@ const INDIR_PER_BLOCK  = 4      # number of block pointers per block
 # bitmap on disk, which is done through the WAL.
 def fs_alloc(fs_state) returns bno:
     acquire(?fs_state->bitmap_lock)
-    bno = fs_state->n_bitmap_blocks + len(fs_state->ib_locks)
+    bno = fs_state->n_bitmap_blocks + fs_state->n_inode_blocks
     var found = False
     while not found:
         bno += 1
@@ -170,6 +170,7 @@ def file_init(n_files) returns req_q:
         let fs_state = malloc({
                 .disk: d, .req_q: req_q, .bitmap_lock: Lock(),
                 .n_bitmap_blocks: n_bitmap_blocks,
+                .n_inode_blocks: n_inode_blocks,
                 .bitmap: [ i <= (1 + n_bitmap_blocks + n_inode_blocks)
                                         for i in { 0 .. N_BLOCKS - 1 } ],
                 .ib_locks: [ RWlock(), ] * n_inode_blocks }):

harmony_model_checker/harmony/behavior.py

@@ -2,6 +2,7 @@
 import sys
 import json
 from typing import Any, Dict, List, Optional, Set, Tuple
+from threading import Thread
 
 from harmony_model_checker.harmony.jsonstring import json_string
 from harmony_model_checker.iface import Transitions_t
@@ -227,6 +228,12 @@ def eps_closure(states: Set[str], transitions: Transitions_t, current: str):
     eps_closure_rec(states, transitions, current, x)
     return frozenset(x)
 
+minified_dfa = None
+
+def do_minify(intermediate_dfa):
+    global minified_dfa
+    minified_dfa = intermediate_dfa.minify(retain_names = True)
+
 def behavior_parse(js, minify, outputfiles, behavior):
     if outputfiles["hfa"] is None and outputfiles["png"] is None and outputfiles["gv"] is None and behavior is None:
         return
@@ -305,9 +312,17 @@ def add_edge(src, val, dst):
         if minify and len(final_states) != 0:
             if len(intermediate_dfa.states) > 100: 
                 print("    * minify #states=%d"%len(intermediate_dfa.states))
-            dfa = intermediate_dfa.minify(retain_names = True)
-            if len(intermediate_dfa.states) > 100: 
-                print("    * minify done #states=%d"%len(dfa.states))
+            thread = Thread(target=do_minify, args=(intermediate_dfa,))
+            thread.start()
+            thread.join(10)
+            if thread.is_alive():
+                print("    * minify: taking too long and giving up")
+                dfa = intermediate_dfa
+            else:
+                global minified_dfa
+                dfa = minified_dfa
+                if len(intermediate_dfa.states) > 100: 
+                    print("    * minify done #states=%d"%len(dfa.states))
         else:
             dfa = intermediate_dfa
         dfa_states = dfa.states
@@ -436,15 +451,19 @@ def add_edge(src, val, dst):
             print("}", file=fd)
 
     if outputfiles["png"] is not None:
-        if got_pydot and got_automata:
-            behavior_show_diagram(dfa, path=outputfiles["png"])
+        if len(dfa.states) > 100:
+            print("    * output of png file suppressed (too many states)") 
         else:
-            assert outputfiles["gv"] is not None
-            try:
-                subprocess.run(["dot", "-Tpng", "-o", outputfiles["png"],
-                                outputfiles["gv"] ])
-            except FileNotFoundError:
-                print("install graphviz (www.graphviz.org) to see output DFAs")
+            if got_pydot and got_automata:
+                behavior_show_diagram(dfa, path=outputfiles["png"])
+            else:
+                print("    * running dot", len(dfa.states))
+                assert outputfiles["gv"] is not None
+                try:
+                    subprocess.run(["dot", "-Tpng", "-o", outputfiles["png"],
+                                    outputfiles["gv"] ])
+                except FileNotFoundError:
+                    print("install graphviz (www.graphviz.org) to see output DFAs")
 
     if behavior is not None:
         if got_automata:

harmony_model_checker/main.py

@@ -3,6 +3,7 @@
 import pathlib
 import webbrowser
 import sys
+import os
 import argparse
 
 from antlr4 import * # type: ignore
@@ -170,6 +171,7 @@ def handle_hco(ns, output_files):
         print("open " + url + " for detailed information, or use the HarmonyGUI", file=sys.stderr)
         if not disable_browser:
             webbrowser.open(url)
+    os._exit(0)     # exit as minify may still be running
 
 def handle_version(_: argparse.Namespace):
     print("Version:", harmony_model_checker.__package__,

harmony_model_checker/modules/synchS.hny

@@ -85,18 +85,19 @@ def V(sema):
 def Queue():
     result = { .list: [], .waiters: [] }
 
-def get(q):
+def get(q) returns next:
     atomically:
         if q->list == []:
-            stop ?q->waiters[len q->waiters]
-
-        result = list.head(q->list)
-        q->list = list.tail(q->list)
+            next = stop ?q->waiters[len q->waiters]
+        else:
+            next = list.head(q->list)
+            q->list = list.tail(q->list)
 
 def put(q, item):
     atomically:
-        q->list = list.append(q->list, item)
         let waiters = q->waiters:
-            if waiters != []:
+            if waiters == []:
+                q->list = list.append(q->list, item)
+            else:
                 go (waiters[0]) item
                 q->waiters = list.tail(waiters)

nworkers.py

@@ -145,7 +145,7 @@ def normalize(lst):
 plt.figure(figsize=(5,2))
 # plt.xscale("log")
 # plt.xticks([1, 2, 4, 8, 16, 32, 64], ["1", "2", "4", "8", "16", "32", "64"])
-plt.xlabel("#threads")
+plt.xlabel("#worker threads")
 plt.ylabel("speed-up")
 dim = np.arange(1, 65)
 

runall.py

@@ -91,6 +91,12 @@
     { "args": "code/abptest.hny", "issue": "No issues", "nstates": 2778 },
     { "args": "code/leader.hny", "issue": "No issues", "nstates": 33005 },
     { "args": "code/2pc.hny", "issue": "No issues", "nstates": 666316 },
+    { "args": "-o reg.hfa code/abdtest.hny", "issue": "No issues", "nstates": 148 },
+    { "args": "-B reg.hfa -mregister=abd code/abdtest.hny", "issue": "No issues", "nstates": 7449569 },
+    { "args": "-o consensus.hfa code/consensus.hny", "issue": "No issues", "nstates": 2602 },
+    { "args": "-B consensus.hfa code/bosco.hny", "issue": "No issues", "nstates": 5288 },
+    { "args": "-o consensus.hfa -cN=2 code/consensus.hny", "issue": "No issues", "nstates": 108 },
+    { "args": "-B consensus.hfa code/paxos.hny", "issue": "No issues", "nstates": 103824 },
     { "args": "-o rsm.hfa code/rsm.hny", "issue": "No issues", "nstates": 1952 },
     { "args": "-B rsm.hfa code/chain.hny", "issue": "No issues", "nstates": 201408 },
     { "args": "code/needhamschroeder.hny", "issue": "Safety violation", "nstates": 558 },