From 9a23df93e6785ad2016a9e6e2d5c737691f8a907 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 13 Feb 2015 13:48:51 -0800 Subject: [PATCH] changes to mcs-lock note --- mcs-lock/note.txt | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/mcs-lock/note.txt b/mcs-lock/note.txt index ef56cdc..aeef26e 100644 --- a/mcs-lock/note.txt +++ b/mcs-lock/note.txt @@ -12,3 +12,14 @@ the gate and the later update of gate. From the inference analysis, we actually got two results, where wildcard(7) and wildcard(8) only need one acquire. That's actually the place to synchronize the update of gate. We can achieve it at the Tail or at the next field. + +To generate those results, we actually need to pass a specific option to the +scfence analysis, as follows. + +******************************************************* +peizhaoo@dw-2:~/model-checker$ ./run.sh mcs-lock/testcase1 -m2 -b100 -y -tSCFENCE -o m +******************************************************* + +The '-b100' is to terminate the execution in case of infinite loops because of +improper synchronization at the beginning period. The 'm' option for SCFENCE +analysis is to turn on the implyMO mode. -- 2.34.1