Skip to content

Commit 810b3ca

Browse files
rvanrenrvanren
committed
Cleaner abort after analysis timeout
1 parent a41635a commit 810b3ca

File tree

4 files changed

+42
-20
lines changed

4 files changed

+42
-20
lines changed

‎harmony_model_checker/charm/charm.c‎

Lines changed: 26 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2684,7 +2684,7 @@ static inline bool report_time(){
26842684
printf("Timeout exceeded during final analysis, disabling some features\n");
26852685
printf("(DFA generation, checking for missing behaviors, ...)\n");
26862686
printf("The timeout can be set with the -X flag\n");
2687-
exit(0);
2687+
global.abort_analysis = true;
26882688
}
26892689
if (now - global.last_report > 3) {
26902690
if (global.lazy_header != NULL) {
@@ -3732,6 +3732,9 @@ static void tarjan(){
37323732
printf(" Node %u\n", n->id);
37333733
report = 0;
37343734
}
3735+
if (global.abort_analysis) {
3736+
return;
3737+
}
37353738
if (pi == 0) {
37363739
scc[n->id].index = i;
37373740
scc[n->id].lowlink = i;
@@ -3771,6 +3774,9 @@ static void tarjan(){
37713774
fflush(stdout);
37723775
lastdone = ndone;
37733776
}
3777+
if (global.abort_analysis) {
3778+
return;
3779+
}
37743780
struct node *n2 = stack_pop(&stack, NULL);
37753781
n2->on_stack = false;
37763782
scc[n2->id].component = comp_id;
@@ -3908,6 +3914,9 @@ static void tarjan_epsclosure(){
39083914
printf(" Node %u\n", n->id);
39093915
report = 0;
39103916
}
3917+
if (global.abort_analysis) {
3918+
return;
3919+
}
39113920
if (pi == 0) {
39123921
scc[n->id].index = i;
39133922
scc[n->id].lowlink = i;
@@ -4323,6 +4332,9 @@ static unsigned int nfa2dfa(FILE *hfa, struct dict *symbols){
43234332
// Pacifier
43244333
work_ctr++;
43254334
if (work_ctr % 10000 == 0 && report_time()) {
4335+
if (global.abort_analysis) {
4336+
return 0;
4337+
}
43264338
printf(" Round %u, partition %u\n", round, n_new);
43274339
}
43284340

@@ -5623,12 +5635,19 @@ int exec_model_checker(int argc, char **argv){
56235635
phase_start("Epsilon closure prep");
56245636
epsilon_closure_prep(); // move epsilon edges to start of each node
56255637
phase_finish();
5626-
phase_start("Epsilon closure");
5627-
tarjan_epsclosure();
5628-
phase_finish();
5629-
printf("* Phase 4c: convert NFA to DFA\n");
5630-
fflush(stdout);
5631-
dfasize = nfa2dfa(hfa, symbols);
5638+
if (!global.abort_analysis) {
5639+
phase_start("Epsilon closure");
5640+
tarjan_epsclosure();
5641+
phase_finish();
5642+
}
5643+
if (!global.abort_analysis) {
5644+
printf("* Phase 4c: convert NFA to DFA\n");
5645+
fflush(stdout);
5646+
dfasize = nfa2dfa(hfa, symbols);
5647+
}
5648+
else {
5649+
fprintf(hfa, " \"status\": \"aborted\"\n");
5650+
}
56325651
}
56335652
else {
56345653
fprintf(hfa, " \"initial\": \"0\",\n");

‎harmony_model_checker/charm/charm.h‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,8 @@ struct global {
108108
bool do_not_pin; // don't pin workers
109109
double last_report; // used for periodic reporting
110110
double report_timeout; // to abort very long reports
111-
double timeout; // -T flag
111+
double timeout; // -X flag
112+
bool abort_analysis; // set after timeout
112113
char *lazy_header; // report header
113114
double start_model_checking; // time when model checking started
114115

‎harmony_model_checker/harmony/behavior.py‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ def read_hfa_file(file):
2929
try:
3030
with open(file, encoding='utf-8') as fd:
3131
js = json.load(fd, strict=False)
32+
if "initial" not in js:
33+
return False
3234
initial = js["initial"]
3335
states = set()
3436
final = set()

‎runall.py‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@
3939
{ "args": "-mqueueconc=queue_lock code/queue_test_seq.hny", "issue": "No issues", "nstates": 15 },
4040
{ "args": "-mqueueconc=queue_MS code/queue_test_seq.hny", "issue": "No issues", "nstates": 16 },
4141
{ "args": "-o queue4.hfa code/queue_btest1.hny", "issue": "No issues", "nstates": 3385 },
42-
{ "args": "-B queue4.hfa -m queue=queue_lock code/queue_btest1.hny", "issue": "No issues", "nstates": 66530 },
43-
{ "args": "-B queue4.hfa -m queue=queue_MS code/queue_btest1.hny", "issue": "No issues", "nstates": 99816 },
42+
{ "args": "-X15 -B queue4.hfa -m queue=queue_lock code/queue_btest1.hny", "issue": "No issues", "nstates": 66530 },
43+
{ "args": "-X15 -B queue4.hfa -m queue=queue_MS code/queue_btest1.hny", "issue": "No issues", "nstates": 99816 },
4444
{ "args": "-mqueue=queue_broken2 code/queue_btest1.hny", "issue": "Safety violation", "nstates": 23875 },
4545
{ "args": "code/rwlock_test1.hny", "issue": "No issues", "nstates": 499 },
4646
{ "args": "-mrwlock=rwlock_sbs code/rwlock_test1.hny", "issue": "No issues", "nstates": 8089 },
@@ -53,11 +53,11 @@
5353
{ "args": "-mrwlock=rwlock_sbs_fair code/rwlock_test1.hny", "issue": "No issues", "nstates": 5831 },
5454
{ "args": "-mrwlock=rwlock_sbs_fair -msynch=synchS code/rwlock_test1.hny", "issue": "No issues", "nstates": 21060 },
5555
{ "args": "-o rw.hfa -cNOPS=3 code/rwlock_btest.hny", "issue": "No issues", "nstates": 2922 },
56-
{ "args": "-B rw.hfa -cNOPS=3 -m rwlock=rwlock_sbs code/rwlock_btest.hny", "issue": "No issues", "nstates": 3018 },
57-
{ "args": "-B rw.hfa -cNOPS=3 -m rwlock=rwlock_cv code/rwlock_btest.hny", "issue": "No issues", "nstates": 2593 },
58-
{ "args": "-B rw.hfa -cNOPS=3 -m rwlock=rwlock_cv_fair code/rwlock_btest.hny", "issue": "No issues", "nstates": 4191 },
59-
{ "args": "-B rw.hfa -cNOPS=3 -m rwlock=rwlock_sbs_fair code/rwlock_btest.hny", "issue": "No issues", "nstates": 2124 },
60-
{ "args": "-B rw.hfa -cNOPS=3 -m rwlock=rwlock_cheat code/rwlock_btest.hny", "issue": "No issues", "nstates": 255 },
56+
{ "args": "-X15 -B rw.hfa -cNOPS=3 -m rwlock=rwlock_sbs code/rwlock_btest.hny", "issue": "No issues", "nstates": 3018 },
57+
{ "args": "-X15 -B rw.hfa -cNOPS=3 -m rwlock=rwlock_cv code/rwlock_btest.hny", "issue": "No issues", "nstates": 2593 },
58+
{ "args": "-X15 -B rw.hfa -cNOPS=3 -m rwlock=rwlock_cv_fair code/rwlock_btest.hny", "issue": "No issues", "nstates": 4191 },
59+
{ "args": "-X15 -B rw.hfa -cNOPS=3 -m rwlock=rwlock_sbs_fair code/rwlock_btest.hny", "issue": "No issues", "nstates": 2124 },
60+
{ "args": "-X15 -B rw.hfa -cNOPS=3 -m rwlock=rwlock_cheat code/rwlock_btest.hny", "issue": "No issues", "nstates": 255 },
6161
{ "args": "-mboundedbuffer=boundedbuffer_hoare code/boundedbuffer_test1.hny", "issue": "No issues", "nstates": 1017 },
6262
{ "args": "-mboundedbuffer=boundedbuffer_hoare -msynch=synchS code/boundedbuffer_test1.hny", "issue": "No issues", "nstates": 4019 },
6363
{ "args": "code/qsorttest.hny", "issue": "No issues", "nstates": 1190 },
@@ -74,7 +74,7 @@
7474
{ "args": "-mbarrier=code/barrier_cv code/barrier_test.hny", "issue": "No issues", "nstates": 5801 },
7575
{ "args": "-mbarrier=code/barrier_cv -msynch=synchS code/barrier_test.hny", "issue": "No issues", "nstates": 13082 },
7676
# { "args": "-o file.hfa code/file_btest.hny", "issue": "No issues", "nstates": 36887 },
77-
# { "args": "-B file.hfa -m file=file_inode code/file_btest.hny", "issue": "No issues", "nstates": 43554096 },
77+
# { "args": "-X15 -B file.hfa -m file=file_inode code/file_btest.hny", "issue": "No issues", "nstates": 43554096 },
7878
{ "args": "code/trap.hny", "issue": "No issues", "nstates": 8 },
7979
{ "args": "code/trap2.hny", "issue": "Safety violation", "nstates": 21 },
8080
{ "args": "code/trap3.hny", "issue": "Non-terminating state", "nstates": 11 },
@@ -87,13 +87,13 @@
8787
{ "args": "code/leader.hny", "issue": "No issues", "nstates": 33005 },
8888
{ "args": "code/2pc.hny", "issue": "No issues", "nstates": 666316 },
8989
{ "args": "-o reg.hfa code/abdtest.hny", "issue": "No issues", "nstates": 148 },
90-
# { "args": "-B reg.hfa -mregister=abd code/abdtest.hny", "issue": "No issues", "nstates": 7449569 },
90+
{ "args": "-X15 -B reg.hfa -mregister=abd code/abdtest.hny", "issue": "No issues", "nstates": 7449569 },
9191
{ "args": "-o consensus.hfa code/consensus.hny", "issue": "No issues", "nstates": 2602 },
92-
{ "args": "-B consensus.hfa code/bosco.hny", "issue": "No issues", "nstates": 5288 },
92+
{ "args": "-X15 -B consensus.hfa code/bosco.hny", "issue": "No issues", "nstates": 5288 },
9393
{ "args": "-o consensus.hfa -cN=2 code/consensus.hny", "issue": "No issues", "nstates": 108 },
94-
{ "args": "-B consensus.hfa code/paxos.hny", "issue": "No issues", "nstates": 103824 },
94+
{ "args": "-X15 -B consensus.hfa code/paxos.hny", "issue": "No issues", "nstates": 103824 },
9595
{ "args": "-o rsm.hfa code/rsm.hny", "issue": "No issues", "nstates": 1952 },
96-
{ "args": "-B rsm.hfa code/chain.hny", "issue": "No issues", "nstates": 213285 },
96+
{ "args": "-X15 -B rsm.hfa code/chain.hny", "issue": "No issues", "nstates": 213285 },
9797
{ "args": "code/needhamschroeder.hny", "issue": "Safety violation", "nstates": 558 },
9898
{ "args": "-mstack=stack1 code/stacktest.hny", "issue": "No issues", "nstates": 2 },
9999
{ "args": "-mstack=stack2 code/stacktest.hny", "issue": "No issues", "nstates": 2 },

0 commit comments

Comments
 (0)