From ad7b37d22da8d7fab4aa70ec947a2c93e55959c8 Mon Sep 17 00:00:00 2001 From: Robbert van Renesse Date: Tue, 22 Aug 2023 11:56:02 -0400 Subject: [PATCH] Working on improving regression test --- harmony_model_checker/charm/charm.c | 1 + runall.py | 115 ++++++++++++++++++++++++++++ runall.scr | 1 - 3 files changed, 116 insertions(+), 1 deletion(-) create mode 100644 runall.py diff --git a/harmony_model_checker/charm/charm.c b/harmony_model_checker/charm/charm.c index 1ecb5a06..1d41d327 100644 --- a/harmony_model_checker/charm/charm.c +++ b/harmony_model_checker/charm/charm.c @@ -4017,6 +4017,7 @@ int exec_model_checker(int argc, char **argv){ assert(global->pretty->type == JV_LIST); fprintf(out, "{\n"); + fprintf(out, " \"nstates\": %d,\n", global->graph.size); // In case no issues were found, we output a summary of the Kripke structure // with the 'print' outputs. diff --git a/runall.py b/runall.py new file mode 100644 index 00000000..92f4a8ad --- /dev/null +++ b/runall.py @@ -0,0 +1,115 @@ +import subprocess +import time +import json +import os.path + +tests = [ + { "args": "code/triangle.hny", "issue": "No issues", "nstates": 13 }, + { "args": "code/prog1.hny", "issue": "No issues", "nstates": 2 }, + { "args": "code/prog2.hny", "issue": "Safety violation", "nstates": 11 }, + { "args": "code/Up.hny", "issue": "Safety violation", "nstates": 44 }, + { "args": "code/Upf.hny", "issue": "Finally predicate violation", "nstates": 13 }, + { "args": "code/UpEnter.hny", "issue": "Non-terminating state", "nstates": 59 }, + { "args": "code/csbarebones.hny", "issue": "Safety violation", "nstates": 5 }, + { "args": "code/cs.hny", "issue": "Safety violation", "nstates": 11 }, + { "args": "code/naiveLock.hny", "issue": "Safety violation", "nstates": 34 }, + { "args": "code/naiveFlags.hny", "issue": "Non-terminating state", "nstates": 45 }, + { "args": "code/naiveTurn.hny", "issue": "Non-terminating state", "nstates": 28 }, + { "args": "code/Peterson.hny", "issue": "No issues", "nstates": 104 }, + { "args": "code/PetersonBroken.hny", "issue": "Safety violation", "nstates": 126 }, + { "args": "code/PetersonInductive.hny", "issue": "Safety violation", "nstates": 4 }, + { "args": "code/csonebit.hny", "issue": "Active busy waiting", "nstates": 73 }, + { "args": "code/PetersonMethod.hny", "issue": "No issues", "nstates": 104 }, + { "args": "code/hanoi.hny", "issue": "Safety violation", "nstates": 28 }, + { "args": "code/clock.hny", "issue": "Safety violation", "nstates": 5462 }, + { "args": "code/cssynch.hny", "issue": "No issues", "nstates": 35 }, + { "args": "-msynch=synchS code/cssynch.hny", "issue": "No issues", "nstates": 58 }, + { "args": "-msynch=ticket code/cssynch.hny", "issue": "No issues", "nstates": 458 }, + { "args": "code/UpLock.hny", "issue": "No issues", "nstates": 48 }, + { "args": "-msynch=synchS code/UpLock.hny", "issue": "No issues", "nstates": 58 }, + { "args": "code/spinlock.hny", "issue": "No issues", "nstates": 473 }, + { "args": "code/xy.hny", "issue": "Safety violation", "nstates": 19 }, + { "args": "code/atm.hny", "issue": "Safety violation", "nstates": 128 }, + { "args": "code/queuedemo.hny", "issue": "No issues", "nstates": 80 }, + { "args": "code/setobjtest.hny", "issue": "No issues", "nstates": 217 }, + { "args": "-msetobj=linkedlist code/setobjtest.hny", "issue": "No issues", "nstates": 9495 }, + { "args": "code/qtestseq.hny", "issue": "No issues", "nstates": 600 }, + { "args": "-mqueueconc=queueMS code/qtestseq.hny", "issue": "No issues", "nstates": 702 }, + { "args": "code/qtest1.hny", "issue": "No issues", "nstates": 202 }, + { "args": "code/qtest2.hny", "issue": "No issues", "nstates": 55 }, + { "args": "code/qtest3.hny", "issue": "No issues", "nstates": 3225 }, + { "args": "code/qtest4.hny", "issue": "No issues", "nstates": 10 }, + { "args": "code/qtestconc.hny", "issue": "No issues", "nstates": 1879206 }, + { "args": "-msynch=synchS code/qtestconc.hny", "issue": "No issues", "nstates": 3430951 }, + { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 }, + { "args": "-B queue4.hfa -m queue=queueconc code/qtestpar.hny", "issue": "No issues", "nstates": 66530 }, + { "args": "-o queue4.hfa code/qtestpar.hny", "issue": "No issues", "nstates": 3385 }, + { "args": "-B queue4.hfa -m queue=queueMS code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 }, + { "args": "-mqueue=queuebroken code/qtestpar.hny", "issue": "Safety violation", "nstates": 5 }, + { "args": "code/RWtest.hny", "issue": "No issues", "nstates": 135 }, + { "args": "-mRW=RWsbs code/RWtest.hny", "issue": "No issues", "nstates": 1757 }, + { "args": "-mRW=RWcv code/RWtest.hny", "issue": "No issues", "nstates": 1691 }, + { "args": "-mRW=RWcv -msynch=synchS code/RWtest.hny", "issue": "No issues", "nstates": 4301 }, + { "args": "-mRW=RWfair code/RWtest.hny", "issue": "No issues", "nstates": 1248 }, + { "args": "-mRW=RWfair -msynch=synchS code/RWtest.hny", "issue": "No issues", "nstates": 3137 }, + { "args": "-o rw.hfa -cNOPS=2 code/RWbtest.hny", "issue": "No issues", "nstates": 273 }, + { "args": "-B rw.hfa -cNOPS=2 -m RW=RWsbs code/RWbtest.hny", "issue": "No issues", "nstates": 1393 }, + { "args": "-o rw.hfa -cNOPS=2 code/RWbtest.hny", "issue": "No issues", "nstates": 273 }, + { "args": "-B rw.hfa -cNOPS=2 -m RW=RWcv code/RWbtest.hny", "issue": "No issues", "nstates": 923 }, + { "args": "-B rw.hfa -cNOPS=2 -m RW=RWfair code/RWbtest.hny", "issue": "No issues", "nstates": 1019 }, + { "args": "-B rw.hfa -cNOPS=2 -m RW=RWcheat code/RWbtest.hny", "issue": "No issues", "nstates": 257 }, + { "args": "-mboundedbuffer=BBhoare code/BBtest.hny", "issue": "No issues", "nstates": 1017 }, + { "args": "-mboundedbuffer=BBhoare -msynch=synchS code/BBtest.hny", "issue": "No issues", "nstates": 4019 }, + { "args": "code/qsorttest.hny", "issue": "No issues", "nstates": 1190 }, + { "args": "code/Diners.hny", "issue": "Non-terminating state", "nstates": 9095 }, + { "args": "-msynch=synchS code/Diners.hny", "issue": "Non-terminating state", "nstates": 32476 }, + { "args": "code/DinersCV.hny", "issue": "No issues", "nstates": 101549 }, + { "args": "-msynch=synchS code/DinersCV.hny", "issue": "No issues", "nstates": 2293519 }, + { "args": "code/DinersAvoid.hny", "issue": "No issues", "nstates": 39884 }, + { "args": "-msynch=synchS code/DinersAvoid.hny", "issue": "No issues", "nstates": 152874 }, + { "args": "code/bank.hny", "issue": "Non-terminating state", "nstates": 2827 }, + { "args": "code/counter.hny", "issue": "No issues", "nstates": 508 }, + { "args": "code/qbarrier.hny", "issue": "No issues", "nstates": 1664 }, + { "args": "-msynch=synchS code/qbarrier.hny", "issue": "No issues", "nstates": 4927 }, + { "args": "code/barriertest.hny", "issue": "No issues", "nstates": 2529 }, + { "args": "-msynch=synchS code/barriertest.hny", "issue": "No issues", "nstates": 7425 }, + { "args": "code/barriertest2.hny", "issue": "No issues", "nstates": 5711 }, + { "args": "-msynch=synchS code/barriertest2.hny", "issue": "No issues", "nstates": 16511 }, + { "args": "code/trap.hny", "issue": "No issues", "nstates": 8 }, + { "args": "code/trap2.hny", "issue": "Finally predicate violation", "nstates": 21 }, + { "args": "code/trap3.hny", "issue": "Non-terminating state", "nstates": 26 }, + { "args": "code/trap4.hny", "issue": "No issues", "nstates": 16 }, + { "args": "code/trap5.hny", "issue": "No issues", "nstates": 16 }, + { "args": "code/trap6.hny", "issue": "No issues", "nstates": 386 }, + { "args": "-msynch=synchS code/trap6.hny", "issue": "No issues", "nstates": 554 }, + { "args": "code/hw.hny", "issue": "No issues", "nstates": 23864 }, + { "args": "code/abptest.hny", "issue": "No issues", "nstates": 2778 }, + { "args": "code/leader.hny", "issue": "Safety violation", "nstates": 117 }, + { "args": "-mstack=stack1 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, + { "args": "-mstack=stack2 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, + { "args": "-mstack=stack3 code/stacktest.hny", "issue": "No issues", "nstates": 2 }, + { "args": "-mstack=stack4 code/stacktest.hny", "issue": "No issues", "nstates": 2 } +] + +for t in tests: + print() + print("Running harmony %s"%t["args"], flush=True) + start = time.time() + args = t["args"].split(" ") + cp = subprocess.run(["./harmony", "--noweb"] + args, capture_output=True) + end = time.time() + if cp.returncode == 0: + (base, ext) = os.path.splitext(args[-1]) + with open(base + ".hco") as f: + hco = json.load(f) + print("time=%.2f, #states=%d, issue=%s" % (end - start, hco["nstates"], hco["issue"])) + if t["issue"] != hco["issue"]: + print("Different issue (was %s)??? Aborting further tests" % t["issue"]) + break + if min(t["nstates"], hco["nstates"]) / max(t["nstates"], hco["nstates"]) < .9: + print("#states very different (was %d)??? Aborting further tests" % t["nstates"]) + else: + print("Error code %d, aborting further tests" % cp.returncode) + print("Output: ", cp.stdout) + print("Error: ", cp.stderr) + break diff --git a/runall.scr b/runall.scr index c4a240e9..71b0c7ff 100755 --- a/runall.scr +++ b/runall.scr @@ -397,4 +397,3 @@ $HARMONY --noweb -mstack=stack1 code/stacktest.hny $HARMONY --noweb -mstack=stack2 code/stacktest.hny $HARMONY --noweb -mstack=stack3 code/stacktest.hny $HARMONY --noweb -mstack=stack4 code/stacktest.hny -