ARC model specified in spinroot/promela

[Mathew, Cherry G.*]

Hello hackers,

I'm writing to introduce a project I've been working on off-and-on for a
while now - verifying parts of kernel code using a formal specifier[1]

Please find attached a patch to try out a formal verification run of the
Adaptive Replacement Cache by Megido et.al. [2]

You can try it out by installing spin from your favourite package
manager, and then running "make" in the current directory - it just
needs the usual C toolchain, afaik.

I'm hoping that someone can help me complete the current run, as I don't
have the computing resources required to run the full model (about 16GB
RAM). Meanwhile I'll keep finding ways to reduce the statespace
required.

The idea here is that once verified, the model can be written up as C
code, and then re-exracted using the modex [3] tool

I have some unpublished work that demonstrates this using the md(4)
NetBSD driver, but I want to be able to do a clean-room implementation
first, in order to get a better sense of a developer methodology I'm
going to call "DDD" or "D3" (Design Driven Development).

Bricks and boquets welcome. (Please Cc: me, as I am not subscribed to
the ML)

[1] https://spinroot.com/spin/whatispin.html
[2] https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf Fig. 4
[3] http://spinroot.com/modex/MANUAL.html

Best,

[Alexander Leidinger]

Post by Mathew, Cherry G.*
Hello hackers,
I'm writing to introduce a project I've been working on off-and-on for a
while now - verifying parts of kernel code using a formal specifier[1]
Please find attached a patch to try out a formal verification run of the
Adaptive Replacement Cache by Megido et.al. [2]
You can try it out by installing spin from your favourite package
manager, and then running "make" in the current directory - it just
needs the usual C toolchain, afaik.
I'm hoping that someone can help me complete the current run, as I don't
have the computing resources required to run the full model (about 16GB
RAM). Meanwhile I'll keep finding ways to reduce the statespace
required.

How long is this supposed to take? For me it took about 2 seconds to
finish.
Note, the Makefile specifies a NetBSD src directory which I don't have
on this FreeBSD system...

Samstag, 02. September 2023, 10:18:12
(235) ***@ttypts/3 # make
cp arc.pml model #mimic modex
cat arc.drv > spinmodel.pml;cat model >> spinmodel.pml;cat arc.inv >>
spinmodel.pml;
spin -a spinmodel.pml
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5))
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) &&
((len(B2.item_list)<=5))))) && (<> ((p>0)))

Samstag, 02. September 2023, 10:18:14
(236) ***@ttypts/3 # ll
total 275
-rw-r--r-- 1 root wheel 1,1K 2 Sep. 10:18 _spin_nvr.tmp
-rw-r--r-- 1 root wheel 2,6K 2 Sep. 10:15 arc.drv
-rw-r--r-- 1 root wheel 555B 2 Sep. 10:15 arc.inv
-rw-r--r-- 1 root wheel 4,6K 2 Sep. 10:15 arc.pml
-rw-r--r-- 1 root wheel 3,3K 2 Sep. 10:15 Makefile
-rw-r--r-- 1 root wheel 4,6K 2 Sep. 10:18 model
-rw-r--r-- 1 root wheel 2,9K 2 Sep. 10:18 pan.b
-rw-r--r-- 1 root wheel 335K 2 Sep. 10:18 pan.c
-rw-r--r-- 1 root wheel 18K 2 Sep. 10:18 pan.h
-rw-r--r-- 1 root wheel 42K 2 Sep. 10:18 pan.m
-rw-r--r-- 1 root wheel 55K 2 Sep. 10:18 pan.p
-rw-r--r-- 1 root wheel 30K 2 Sep. 10:18 pan.t
-rw-r--r-- 1 root wheel 7,8K 2 Sep. 10:18 spinmodel.pml

Bye,
Alexander.

[Mathew, Cherry G.*]

Hi Alexander,
[...]


AL> How long is this supposed to take? For me it took about 2
AL> seconds to finish.

Apologies, I should have given more detailed instructions.

I've organised the process in three steps:

1) Generate the model from spec: make spin-gen
2) Build the model: make spin-build
3) Run the model: make spin-run

This is the heavy duty part, which takes up quite a bit of vmem (my
process dies at about 8GB due to lack of swap etc. - makes no sense to
thrash it beyond that without RAM - it slows down a lot).

If all goes well with step 3) , then you will see a summary of the run
on console. However, if there was an inconsistency or error detected in
the run, then a tracefile is generated (spinmodel.pml.trail). I've
included a target to dump a human friendly version of this trace.

4) Print trace from debug trail: make spin-trace


AL> Note, the Makefile specifies a NetBSD src directory which I
AL> don't have on this FreeBSD system...

Sorry, I should have mentioned - you can safely ignore that - no
specific external source layout is currently assumed - in fact I run
these tests on a Linux VM at the moment.

The source files become relevant only when the "model extraction" is
done - I haven't got there yet for this project.
ade> For what it's worth, spin is available from ports (devel/spin),
ade> which I've just adopted and updated to 6.5.2, so it is quite
ade> straightforward to get this running on any recent FreeBSD
ade> system.

Hi ade,

Nice! I'd be curious to know performance comparisons viz Linux etc. esp
because there seems to be a threaded version of spin (not sure if the
FreeBSD package build enables this).

ade> I tested only with the ancient Peterson's mutual exclusion,
ade> which resolves instantly. Mailing-list archives don't preserve
ade> attachments, so, Cherry, if you could send it me directly that
ade> would be lovely. I spotted A. Mader's PLC Controller in the
ade> SPIN documents, that is one I am familiar with, and then
ade> realised that academic papers from the 2000s don't come with
ade> source code :(

Thanks, I noticed that after checking the archives, and did send a
second mail with an inline patch. Will also send you a private one after
this.

Thanks so much for your interest - mainly, I'd like to understand how
bad the statespace explosion is for this model. This will help me get a
sense of what complexity of models we can attempt to verify like this,
with current "commodity" hardware.

Many Thanks,

[Alexander Leidinger]

Post by Mathew, Cherry G.*
Hi Alexander,
[...]
AL> How long is this supposed to take? For me it took about 2
AL> seconds to finish.
Apologies, I should have given more detailed instructions.
1) Generate the model from spec: make spin-gen
2) Build the model: make spin-build
3) Run the model: make spin-run
This is the heavy duty part, which takes up quite a bit of vmem (my
process dies at about 8GB due to lack of swap etc. - makes no sense to
thrash it beyond that without RAM - it slows down a lot).

Seems to be single threaded (Adrian, this is with spin 6.5.0 from an
about 2 days old ports tree). Takes only 1 CPU. After 20min it is at 25G
(20G RES). The system has 64G of RAM and 100G of swap, we will see if
this is enough.

I will report back when it is finished.

Bye,
Alexander.

[Mathew, Cherry G.*]

[...]

Post by Alexander Leidinger
Seems to be single threaded (Adrian, this is with spin 6.5.0 from
an about 2 days old ports tree). Takes only 1 CPU. After 20min it
is at 25G (20G RES). The system has 64G of RAM and 100G of swap,
we will see if this is enough.

Thank you so much for this, and the trace output in the subsequent
email!

So there's room for improvement in my Makefile to:

1) Explore multithreaded/CPU
2) Understand state space explosion scale - it is exponential to the
number of processes, I've fixed it to run in a loop - will report
back once I have good progress also with the model extraction part.
3) My model has errors - I'm glad to see that the error reporting is the
same in my new optimised loop, as in the RAM hungry version you ran.

Thanks once again - this is very helpful. I will report back once I have
more progress.

[Mathew, Cherry G.*]

[...]

Post by Mathew, Cherry G.*
1) Explore multithreaded/CPU
2) Understand state space explosion scale - it is exponential to
the number of processes, I've fixed it to run in a loop - will
report back once I have good progress also with the model
extraction part.
3) My model has errors - I'm glad to see that the error reporting
is the same in my new optimised loop, as in the RAM hungry version
you ran.
Thanks once again - this is very helpful. I will report back once
I have more progress.

Hi Again,

So just wanted to report back with a patch (absolute patch, not relative,
so please nuke your existing arc/ if you tried the old one and apply in
a clean new subdirectory) on the following:

- implemented a loop method to drive the ARC() function runs in a second
at most.
- the model verification caught a logical error in my model! It was
causing an unbounded growth in the T2 directory list.
- expanded the invariants to include several ones described in the
paper.
- cleaned up the "UI" a bit - now you can directly run the verifier
using: "make clean spin-run"

Since the objective here is to demonstrate the dev methodology, I've
left the verifier with a couple of unexplored code/state-paths. See
comments in arc.drv for more on how to fix that. (I will look into this
later).

The next step is to write the equivalent C code, compile it with a
simple test "driver" (ideally ATF, but since this is standalone for the
moment, I'll use something simpler, just to illustrate the concept), and
then hook it into spin's "modex" tool, to extract the implicit
model. Once this is done, we'll have a full cycle of
design->implement->verify and this will demonstrate the DDD (Design
Driven Development) methodology I'd love to hear your thoughts about.

Many Thanks in advance for any ideas, thoughts, critiques, bugs, etc.
--
~cherry

diff -urN arc.null/arc.drv arc/arc.drv
--- arc.null/arc.drv 1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.drv 2023-09-04 10:32:34.042373574 +0000
@@ -0,0 +1,52 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+/* Note: What we're attempting in this driver file, is to generate an
+ * input trace that would exercise all code-paths of the model specified
+ * in arc.pml
+ *
+ * Feeding a static trace to the algorithm in array _x[N_ITEMS] is a
+ * acceptable alternative.
+ */
+#include "arc.pmh"
+
+#define N_ITEMS (2 * C) /* Number of distinct cache items to test with */
+#define ITEM_REPS (C / 4) /* Max repeat item requests */
+#define N_ITERATIONS 3
+
+hidden arc_item _x[N_ITEMS]; /* Input state is irrelevant from a verification PoV */
+hidden int _x_iid = 0;
+hidden int _item_rep = 0;
+hidden byte _iterations = 0;
+
+/* Drive the procs */
+init {
+
+ atomic {
+ do
+ ::
+ _iterations < N_ITERATIONS ->
+
+ _x_iid = 0;
+ do
+ :: _x_iid < N_ITEMS ->
+ init_arc_item(_x[_x_iid], _x_iid, false);
+ _item_rep = 0;
+ do
+ :: _item_rep < (_x_iid % ITEM_REPS) ->
+ ARC(_x[_x_iid]);
+ _item_rep++;
+ :: _item_rep >= (_x_iid % ITEM_REPS) ->
+ break;
+ od
+ _x_iid++;
+ :: _x_iid >= N_ITEMS ->
+ break;
+ od
+ _iterations++;
+ ::
+ _iterations >= N_ITERATIONS ->
+ break;
+ od
+ }
+
+}
diff -urN arc.null/arc.inv arc/arc.inv
--- arc.null/arc.inv 1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.inv 2023-09-04 09:20:20.224107390 +0000
@@ -0,0 +1,59 @@
+/* $NetBSD$ */
+
+/* These are Linear Temporal Logic invariants (and constraints)
+ * applied over the statespace created by the promela
+ * specification. Correctness is implied by Logical consistency.
+ */
+ltl
+{
+ /* Liveness - all threads, except control must finally exit */
+ eventually always (_nr_pr == 1) &&
+ /* c.f Section I. B, on page 3 of paper */
+ always ((lengthof(T1) +
+ lengthof(B1) +
+ lengthof(T2) +
+ lengthof(B2)) <= (2 * C)) &&
+
+ /* Reading together Section III. A., on page 7, and
+ * Section III. B., on pages 7,8
+ */
+ always ((lengthof(T1) + lengthof(B1)) <= C) &&
+ always ((lengthof(T2) + lengthof(B2)) < (2 * C)) &&
+
+ /* Section III. B, Remark III.1 */
+ always ((lengthof(T1) + lengthof(T2)) <= C) &&
+
+ /* TODO: III B, A.1 */
+
+ /* III B, A.2 */
+ always (((lengthof(T1) +
+ lengthof(B1) +
+ lengthof(T2) +
+ lengthof(B2)) < C)
+ implies ((lengthof(B1) == 0) &&
+ lengthof(B2) == 0)) &&
+
+ /* III B, A.3 */
+ always (((lengthof(T1) +
+ lengthof(B1) +
+ lengthof(T2) +
+ lengthof(B2)) >= C)
+ implies ((lengthof(T1) +
+ lengthof(T2) == C))) &&
+
+ /* TODO: III B, A.4 */
+
+ /* TODO: III B, A.5 */
+
+ /* IV A. */
+ always (p <= C) &&
+
+ /* Not strictly true, but these force us to generate a "good"
+ * input trace via arc.drv
+ */
+
+ eventually /* always ? */ ((lengthof(T1) == p) && lengthof(T2) == (C - p)) &&
+
+ eventually (p > 0)
+
+}
diff -urN arc.null/arc.pmh arc/arc.pmh
--- arc.null/arc.pmh 1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.pmh 2023-09-04 10:27:50.069213153 +0000
@@ -0,0 +1,59 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+#ifndef _ARC_INC
+#define _ARC_INC
+
+/* XXX: Move these into a set of library includes ? */
+/* XXX: Equivalence verification */
+/* Note: CAS implemented in an atomic {} block */
+#define mutex_enter(_mutex) \
+ atomic { \
+ (_mutex == 0) -> _mutex = 1; \
+ }
+
+#define mutex_exit(_mutex) \
+ atomic { \
+ assert(_mutex == 1); \
+ (_mutex == 1) -> _mutex = 0; \
+ }
+
+bit sc_lock;
+
+#define C 64 /* Cache size - use judiciously - adds to statespace */
+
+typedef arc_item {
+ int iid; /* Unique identifier for item */
+ bool cached;
+};
+
+/* Note that we use the arc_item.iid as the member lookup handle to reduce state space */
+typedef arc_list {
+ chan item_list = [ 2 * C ] of { int }; /* A list of page items */
+};
+
+#define lengthof(_arc_list) len(_arc_list.item_list)
+#define memberof(_arc_list, _arc_item) _arc_list.item_list??[eval(_arc_item.iid)]
+#define addMRU(_arc_list, _arc_item) _arc_list.item_list!_arc_item.iid
+#define readLRU(_arc_list, _arc_item) _arc_list.item_list?<_arc_item.iid>
+#define delLRU(_arc_list) _arc_list.item_list?_
+#define delitem(_arc_list, _arc_item) _arc_list.item_list??eval(_arc_item.iid)
+#define refreshitemto(_src_arc_list, _dest_arc_list, _arc_item) \
+ d_step { \
+ delitem(_src_arc_list, _arc_item); \
+ addMRU(_dst_arc_list, _arc_item); \
+ }
+#define refreshitem(_arc_list, _arc_item) refreshitemto(_arc_list, _arc_list, _arc_item)
+
+#define cachefetch(_arc_item) _arc_item.cached = true
+#define cacheremove(_arc_item) _arc_item.cached = false
+
+#define min(a, b) ((a < b) -> a : b)
+#define max(a, b) ((a > b) -> a : b)
+
+#define init_arc_item(_arc_item, _iid, _cached) \
+ d_step { \
+ _arc_item.iid = _iid; \
+ _arc_item.cached = _cached; \
+ }
+
+#endif /* _ARC_INC_ */
\ No newline at end of file
diff -urN arc.null/arc.pml arc/arc.pml
--- arc.null/arc.pml 1970-01-01 00:00:00.000000000 +0000
+++ arc/arc.pml 2023-09-04 10:15:53.767411900 +0000
@@ -0,0 +1,216 @@
+/* Spin process model for Adaptive Replacement Cache algorithm. Written by cherry */
+
+/*
+ * We implement the following algorithm from page 10, Figure 4.
+ * https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf
+ *
+ *
+ * ARC(c)
+ *
+ * INPUT: The request stream x1,x2,....,xt,....
+ * INITIALIZATION: Set p = 0 and set the LRU lists T1, B1, T2, and B2 to empty.
+ *
+ * For every t>=1 and any xt, one and only one of the following four cases must occur.
+ * Case I: xt is in T1 or T2. A cache hit has occurred in ARC(c) and DBL(2c).
+ * Move xt to MRU position in T2.
+ *
+ * Case II: xt is in B1. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ * ADAPTATION: Update p = min { p + d1,c }
+ * where d1 = { 1 if |B1| >= |B2|, |B2|/|B1| otherwise
+ *
+ * REPLACE(xt, p). Move xt from B1 to the MRU position in T2 (also fetch xt to the cache).
+ *
+ * Case III: xt is in B2. A cache miss (resp. hit) has occurred in ARC(c) (resp. DBL(2c)).
+ * ADAPTATION: Update p = max { p - d2,0 }
+ * where d2 = { 1 if |B2| >= |B1|, |B1|/|B2| otherwise
+ *
+ * REPLACE(xt, p). Move xt from B2 to the MRU position in T2 (also fetch xt to the cache).
+ *
+ * Case IV: xt is not in T1 U B1 U T2 U B2. A cache miss has occurred in ARC(c) and DBL(2c).
+ * Case A: L1 = T1 U B1 has exactly c pages.
+ * If (|T1| < c)
+ * Delete LRU page in B1. REPLACE(xt,p).
+ * else
+ * Here B1 is empty. Delete LRU page in T1 (also remove it from the cache).
+ * endif
+ * Case B: L1 = T1 U B1 has less than c pages.
+ * If (|T1| + |T2| + |B1| + |B2| >= c)
+ * Delete LRU page in B2, if (|T1| + |T2| + |B1| + |B2| = 2c).
+ * REPLACE(xt, p).
+ * endif
+ *
+ * Finally, fetch xt to the cache and move it to MRU position in T1.
+ *
+ * Subroutine REPLACE(xt,p)
+ * If ( (|T1| is not empty) and ((|T1| exceeds the target p) or (xt is in B2 and |T1| = p)) )
+ * Delete the LRU page in T1 (also remove it from the cache), and move it to MRU position in B1.
+ * else
+ * Delete the LRU page in T2 (also remove it from the cache), and move it to MRU position in B2.
+ * endif
+ */
+
+#include "arc.pmh"
+
+#define IID_INVAL -1 /* XXX: move to header ? */
+
+/* Temp variable to hold LRU item */
+hidden arc_item LRUitem;
+
+/* Adaptation "delta" variables */
+int d1, d2;
+int p = 0;
+
+/* Declare arc lists - "shadow/ghost cache directories" */
+arc_list B1, B2, T1, T2;
+
+inline REPLACE(/* arc_item */ x_t, /* int */ p)
+{
+ /*
+ * Since LRUitem is declared in scope p_ARC, we expect it to be only accessible from there and REPLACE()
+ * as REPLACE() is only expected to be called from p_ARC.
+ * XXX: May need to revisit due to Modex related limitations.
+ */
+ init_arc_item(LRUitem, IID_INVAL, false);
+
+ if
+ ::
+ (lengthof(T1) != 0) &&
+ ((lengthof(T1) > p) || (memberof(B2, x_t) && (lengthof(T1) == p)))
+ ->
+ d_step {
+ readLRU(T1, LRUitem);
+ delLRU(T1);
+ cacheremove(LRUitem);
+ addMRU(B1, LRUitem);
+ }
+
+ ::
+ else
+ ->
+ d_step {
+ readLRU(T2, LRUitem);
+ delLRU(T2);
+ cacheremove(LRUitem);
+ addMRU(B2, LRUitem);
+ }
+ fi
+}
+
+inline ARC(/* arc_item */ x_t)
+{
+ if
+ :: /* Case I */
+ memberof(T1, x_t)
+ ->
+ d_step {
+ delitem(T1, x_t);
+ addMRU(T2, x_t);
+ }
+ :: /* Case I */
+ memberof(T2, x_t)
+ ->
+ d_step {
+ delitem(T2, x_t);
+ addMRU(T2, x_t);
+ }
+ :: /* Case II */
+ memberof(B1, x_t)
+ ->
+ d1 = ((lengthof(B1) >= lengthof(B2)) -> 1 : (lengthof(B2)/lengthof(B1)));
+ p = min((p + d1), C);
+
+ REPLACE(x_t, p);
+ d_step {
+ delitem(B1, x_t);
+ addMRU(T2, x_t);
+ cachefetch(x_t);
+ }
+ :: /* Case III */
+ memberof(B2, x_t)
+ ->
+ d2 = ((lengthof(B2) >= lengthof(B1)) -> 1 : (lengthof(B1)/lengthof(B2)));
+ p = max(p - d2, 0);
+
+ REPLACE(x_t, p);
+ d_step {
+ delitem(B2, x_t);
+ addMRU(T2, x_t);
+ cachefetch(x_t);
+ }
+ :: /* Case IV */
+ !(memberof(T1, x_t) ||
+ memberof(B1, x_t) ||
+ memberof(T2, x_t) ||
+ memberof(B2, x_t))
+ ->
+ if
+ :: /* Case A */
+ ((lengthof(T1) + lengthof(B1)) == C)
+ ->
+ if
+ ::
+ (lengthof(T1) < C)
+ ->
+ delLRU(B1);
+ REPLACE(x_t, p);
+ ::
+ else
+ ->
+ assert(lengthof(B1) == 0);
+ d_step {
+ readLRU(T1, LRUitem);
+ delLRU(T1);
+ cacheremove(LRUitem);
+ }
+ fi
+ :: /* Case B */
+ ((lengthof(T1) + lengthof(B1)) < C)
+ ->
+ if
+ ::
+ ((lengthof(T1) +
+ lengthof(T2) +
+ lengthof(B1) +
+ lengthof(B2)) >= C)
+ ->
+ if
+ ::
+ ((lengthof(T1) +
+ lengthof(T2) +
+ lengthof(B1) +
+ lengthof(B2)) == (2 * C))
+ ->
+ delLRU(B2);
+ ::
+ else
+ ->
+ skip;
+ fi
+ REPLACE(x_t, p);
+ ::
+ else
+ ->
+ skip;
+ fi
+ ::
+ else
+ ->
+ skip;
+ fi
+ cachefetch(x_t);
+ addMRU(T1, x_t);
+ fi
+
+}
+
+#if 0 /* Resolve this after modex extract foo */
+proctype p_arc(arc_item x_t)
+{
+ /* Serialise entry */
+ mutex_enter(sc_lock);
+
+ ARC(x_t);
+
+ mutex_exit(sc_lock);
+}
+#endif
diff -urN arc.null/Makefile arc/Makefile
--- arc.null/Makefile 1970-01-01 00:00:00.000000000 +0000
+++ arc/Makefile 2023-09-04 10:29:48.141325923 +0000
@@ -0,0 +1,72 @@
+# This set of spinroot related files were written by cherry
+# <***@bow.st> in the Gregorian Calendar year AD.2023, in the month
+# of February that year.
+#
+# We have two specification files and a properties file
+#
+# The properties file contains "constraint" sections
+# such as ltl or never claims (either or, not both).
+# The specification is divided into two files:
+# the file with suffix '.drv' is a "driver" which
+# instantiates processes that will ultimately "drive" the
+# models under test.
+# The file with the suffix '.pml' contains the process
+# model code, which, is intended to be the formal specification
+# for the code we are interested in writing in C.
+#
+# We process these files in slightly different ways during
+# the dev cycle, but broadly speaking, the idea is to create
+# a file called 'spinmodel.pml' which contains the final
+# model file that is fed to spin.
+#
+# Note that when we use the model extractor tool "modex" to
+# extract the 'specification' from C code written to implement
+# the model defined above. We use a 'harness' file (see file with
+# suffix '.prx' below.
+#
+# Once the harness has been run, spinmodel.pml should be
+# synthesised and processed as usual.
+#
+# The broad idea is that software dev starts by writing the spec
+# first, validating the model, and then implementing the model in
+# C, after which we come back to extract the model from the C file
+# and cross check our implementation using spin.
+#
+# If things go well, the constraints specified in the '.ltl' file
+# should hold exactly for both the handwritten model, and the
+# extracted one.
+
+spin-gen: arc.pml arc.drv arc.inv
+ cp arc.pml model #mimic modex
+ cat model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> spinmodel.pml;
+ spin -am spinmodel.pml
+
+spin-build: spin-gen
+ cc -DVECTORSZ=65536 -o pan pan.c
+
+all: spin-gen spin-build
+
+# Verification related targets.
+spin-run: spin-build
+ ./pan -a #Generate arc.pml.trail on error
+
+# You run the trace only if the spin run above failed and created a trail
+spin-trace: spinmodel.pml.trail
+ spin -t spinmodel.pml -p -g # -p (statements) -g (globals) -l (locals) -s (send) -r (recv)
+ ./pan -r spinmodel.pml.trail -g
+
+# Housekeeping
+spin-gen-clean:
+ rm -f spinmodel.pml # Our consolidated model file
+ rm -f _spin_nvr.tmp # Never claim file
+ rm -f model # Intermediate "model" file
+ rm -f pan.* # Spin generated source files
+
+spin-build-clean:
+ rm -f pan
+
+spin-run-clean:
+ rm -f spinmodel.pml.trail
+
+clean: spin-gen-clean spin-build-clean spin-run-clean
+ rm -f *~


--
Posted automagically by a mail2news gateway at muc.de e.V.
Please direct questions, flames, donations, etc. to news-***@muc.de

[Alexander Leidinger]

Post by Mathew, Cherry G.*
[...]

Post by Mathew, Cherry G.*
1) Explore multithreaded/CPU
2) Understand state space explosion scale - it is exponential to
the number of processes, I've fixed it to run in a loop - will
report back once I have good progress also with the model
extraction part.
3) My model has errors - I'm glad to see that the error reporting
is the same in my new optimised loop, as in the RAM hungry

version

Post by Mathew, Cherry G.*
you ran.
Thanks once again - this is very helpful. I will report back once
I have more progress.

Hi Again,
So just wanted to report back with a patch (absolute patch, not relative,
so please nuke your existing arc/ if you tried the old one and apply in

# make spin-run
cp arc.pml model #mimic modex
cat model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >>
spinmodel.pml;
spin -am spinmodel.pml
ltl ltl_0: (((((((((<> ([] ((_nr_pr==1)))) && ([]
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<=(2*64)))))
&& ([] (((len(T1.item_list)+len(B1.item_list))<=64)))) && ([]
(((len(T2.item_list)+len(B2.item_list))<(2*64))))) && ([]
(((len(T1.item_list)+len(T2.item_list))<=64)))) && ([] ((!
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<64)))
|| (((len(B1.item_list)==0)) && ((len(B2.item_list)==0)))))) && ([] ((!
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))>=64)))
|| (((len(T1.item_list)+len(T2.item_list))==64))))) && ([] ((p<=64))))
&& (<> (((len(T1.item_list)==p)) && ((len(T2.item_list)==(64-p)))))) &&
(<> ((p>0)))
cc -DVECTORSZ=65536 -o pan pan.c
./pan -a #Generate arc.pml.trail on error
error: max search depth too small

(Spin Version 6.5.0 -- 1 July 2019)
+ Partial Order Reduction

Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 2124 byte, depth reached 9999, errors: 0
1 states, stored
11 states, matched
12 transitions (= stored+matched)
109989 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector
+ overhead))
12.456 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
5.686 memory lost to fragmentation
140.500 total actual memory usage


unreached in init
spinmodel.pml:80, state 28, "D_STEP80"
spinmodel.pml:80, state 53, "D_STEP80"
spinmodel.pml:154, state 70, "B1.item_list?_"
spinmodel.pml:80, state 79, "D_STEP80"
spinmodel.pml:90, state 85, "D_STEP90"
spinmodel.pml:78, state 86,
"(((len(T1.item_list)!=0)&&((len(T1.item_list)>p)||(B2.item_list??[eval(x[x_iid].iid)]&&(len(T1.item_list)==p)))))"
spinmodel.pml:78, state 86, "else"
spinmodel.pml:73, state 88, "D_STEP73"
spinmodel.pml:159, state 90, "assert((len(B1.item_list)==0))"
spinmodel.pml:160, state 94, "D_STEP160"
spinmodel.pml:152, state 95, "((len(T1.item_list)<64))"
spinmodel.pml:152, state 95, "else"
spinmodel.pml:183, state 100, "B2.item_list?_"
spinmodel.pml:198, state 128, "(1)"
spinmodel.pml:268, state 155, "-end-"
(13 of 155 states)
unreached in claim ltl_0
_spin_nvr.tmp:70, state 108, "-end-"
(1 of 108 states)

pan: elapsed time 0.164 seconds
pan: rate 6.0952381 states/second



No trail file generated...

Bye,
Alexander.

[Alexander Leidinger]

A few things remain WIP. Obviously, this is a "toy" model - it has
stack
based "memory" management, and a directory buffer size of 64. So that
needs to be hammered on a bit more. Further, I'm keen to now dip my
toes
into re-entrancy. If you noticed in the earlier patches, there were
model routines for "mutex_enter()/mutex_exit()". I'll re-look these and
play around a little bit with concurrent entry of ARC() (ARC() is now
strictly entered sequentially in a loop - see arc.drv). Once things
settle down, I will look at making an actual block disk driver with an
ARC(9) managed cache using this code.

Without having looked at anything in the code, and now with your comment
about an "actual block disk driver"... AFAIR your ARC is based upon the
paper, and this is not used anywhere in FreeBSD. ZFS is using a
modified/adapted version of the ARC. What you are describing sounds a
bit like our buffer cache
(https://wiki.freebsd.org/BasicVfsConcepts#:~:text=Buffer%20cache%20is%20a%20layer,on%20a%20vnode%2Blbn%20basis.),
but our buffer cache is not an ARC, it is AFAIR LRU eviction based.

I fully understand that you are far away from doing real modelling of
such complex parts as the VFS parts of FreeBSD, but maybe this info
gives a hint in terms of looking into some parts and see if you can
adopt some parts in terms of design which can be anhanced later on to
some real FreeBSD stuff...

Bye,
Alexander.

[Mathew, Cherry G.*]

Post by Alexander Leidinger

A few things remain WIP. Obviously, this is a "toy" model - it
has stack based "memory" management, and a directory buffer size
of 64. So that needs to be hammered on a bit more. Further, I'm
keen to now dip my toes into re-entrancy. If you noticed in the
earlier patches, there were model routines for
"mutex_enter()/mutex_exit()". I'll re-look these and play around
a little bit with concurrent entry of ARC() (ARC() is now
strictly entered sequentially in a loop - see arc.drv). Once
things settle down, I will look at making an actual block disk
driver with an ARC(9) managed cache using this code.

Without having looked at anything in the code, and now with your
comment about an "actual block disk driver"... AFAIR your ARC is
based upon the paper, and this is not used anywhere in
FreeBSD. ZFS is using a modified/adapted version of the ARC. What
you are describing sounds a bit like our buffer cache
(https://wiki.freebsd.org/BasicVfsConcepts#:~:text=Buffer%20cache%20is%20a%20layer,on%20a%20vnode%2Blbn%20basis.),
but our buffer cache is not an ARC, it is AFAIR LRU eviction
based.

Hi Alexander - thank you for the comments! Regarding the buffer cache,
that is an excellent suggestion, and there are a few things that need to
fall in place before it can be meaningfully verified. I'd say that the
first step is to put in place "Equivalence verification" code for all
the backing infrastructure that most kernel code uses - for example
things that mediate or enable concurrency, such as cv(9), mutex(9),
spl(9) (Not sure if that exists in FreeBSD), etc. Once those are in
place, it will be much easier to write model+invariance code with some
measure of confidence, along with extraction. I already have very very
rudimentary code for this that I wrote for a QNX job interview (which,
very puzzlingly, for a project that claims to support critical systems,
they found uninteresting to the point of having zero questions about!) -
the point is - it's actually not that hard to put it together (I did it
over about 20hours of focussed work) and the benefits are enormous, from
what I can tell.

Regarding the "block driver" I'm thinking of - at the moment, in my
head, it's really not that ambitious at all - it's just a self contained
read-cache that could potentially front any existing block driver - for
eg: a super slow spindisk based driver could get potential block level
speed up. I don't know if the buffer cache works in this way, or it
only caches data along specific code paths such as read(2) - this is not
an area of the OS I'm familiar with. But there is no reason why the
buffer cache itself can't be modelled and verified, if it has been
written reasonably carefully enough, modularity wise.

Post by Alexander Leidinger
I fully understand that you are far away from doing real modelling
of such complex parts as the VFS parts of FreeBSD, but maybe this
info gives a hint in terms of looking into some parts and see if
you can adopt some parts in terms of design which can be anhanced
later on to some real FreeBSD stuff...

Definitely noted, and thank you for the signpost! I'm pasting below some
early work I did in February, just to give a sense of what it might look
like, if an existing part of the (in this case NetBSD) kernel were to be
attempted to be verified. Note that the work below is incomplete, but it
did show PoC, which prompted me to investigate this line of reasoning
further.

I'm looking forward to working more in this area, and hope that the
FreeBSD community will have some interest in supporting this work,
especially once the equivalence code is in place, by verifying existing
bits of code piecemeal until we can have the entire OS under at least
a very basic verification harness!

Looking forward.
--
~cherry

diff -urN Makefile ./Makefile
--- Makefile 1970-01-01 05:30:00.000000000 +0530
+++ ./Makefile 2023-02-22 00:51:21.589143403 +0530
@@ -0,0 +1,89 @@
+# This set of spinroot related files were written by cherry
+# <***@bow.st> in the Gregorian Calendar year AD.2023, in the month
+# of February that year.
+#
+# We have two specification files and a properties file
+#
+# The properties file contains "constraint" sections
+# such as ltl or never claims (either or, not both).
+# The specification is divided into two files:
+# the file with suffix '.drv' is a "driver" which
+# instantiates processes that will ultimately "drive" the
+# models under test.
+# The file with the suffix '.pml' contains the process
+# model code, which, is intended to be the formal specification
+# for the code we are interested in writing in C.
+#
+# We process these files in slightly different ways during
+# the dev cycle, but broadly speaking, the idea is to create
+# a file called 'spinmodel.pml' which contains the final
+# model file that is fed to spin.
+#
+# Note that when we use the model extractor tool "modex" to
+# extract the 'specification' from C code written to implement
+# the model defined above. We use a 'harness' file (see file with
+# suffix '.prx' below.
+#
+# Once the harness has been run, spinmodel.pml should be
+# synthesised and processed as usual.
+#
+# The broad idea is that software dev starts by writing the spec
+# first, validating the model, and then implementing the model in
+# C, after which we come back to extract the model from the C file
+# and cross check our implementation using spin.
+#
+# If things go well, the constraints specified in the '.ltl' file
+# should hold exactly for both the handwritten model, and the
+# extracted one.
+
+spin-gen: md.strategy.pml md.strategy.drv md.strategy.prop
+ cp md.strategy.pml model #mimic modex
+ cat md.strategy.drv > spinmodel.pml;cat model >> spinmodel.pml;cat md.strategy.prop >> spinmodel.pml;
+ spin -a spinmodel.pml
+
+spin-build: pan.*
+ cc -o pan pan.c
+
+spin-run: spin-build #XXX depend on pan
+ ./pan -a #Generate md.strategy.pml.trail on error
+
+# You run the trace only if the spin run above failed and created a trail
+spin-trace: spinmodel.pml.trail
+ spin -t spinmodel.pml -p -g # -p (statements) -g (globals) -l (locals) -s (send) -r (recv)
+ ./pan -r spinmodel.pml.trail -g
+
+# Modex Extracts from md.c to 'model' - see md.strategy.prx
+# Unfortunately there doesn't seem to be a way to specify a filename
+# to generate
+SRC = $HOME/work/NetBSD-src
+
+modex-gen: md.strategy.prx md.c
+ #modex -v -w -D_KERNEL -I$obj/home/antix/work/NetBSD-src/destdir.amd64/usr/include -I$$HOME/work/NetBSD-src/obj/home/antix/work/NetBSD-src/sys/arch/amd64/compile/GENERIC/ -I$$HOME/work/NetBSD-src/sys md.strategy.prx
+ #cat model > spinmodel.pml
+ touch ioconf.h # Pretend we have an Kern conf
+ modex -v -w md.strategy.prx
+ cat md.strategy.drv > spinmodel.pml;cat model >> spinmodel.pml;cat md.strategy.prop >> spinmodel.pml;
+ spin -a spinmodel.pml #Sanity check
+
+modex-gen-clean:
+ rm -f ioconf.h # Temp - see above.
+ rm -f spinmodel.pml # Our consolidated model file
+ rm -f _spin_nvr.tmp # Never claim file
+ rm -f model # modex generated intermediate "model" file
+ rm -f pan.* # Spin generated source files
+ rm -f _modex* # modex generated script files
+ rm -f *.I *.M
+spin-gen-clean:
+ rm -f spinmodel.pml # Our consolidated model file
+ rm -f _spin_nvr.tmp # Never claim file
+ rm -f model # Intermediate "model" file
+ rm -f pan.* # Spin generated source files
+
+spin-build-clean:
+ rm -f pan
+
+spin-run-clean:
+ rm -f spinmodel.pml.trail
+
+clean: modex-gen-clean spin-gen-clean spin-build-clean spin-run-clean
+# rm -f *~
diff -urN md.strategy.drv ./md.strategy.drv
--- md.strategy.drv 1970-01-01 05:30:00.000000000 +0530
+++ ./md.strategy.drv 2023-02-22 00:26:27.428777059 +0530
@@ -0,0 +1,211 @@
+/* $NetBSD$ */
+
+/* Spin model driver for NetBSD md(4) md.c written by cherry */
+
+//#define MEMORY_DISK_SERVER
+
+/* XXX: Bitfields are messed up, because promella doesn't do hex */
+
+#define B_WRITE 0 /* Write buffer (pseudo flag). */
+#define B_READ 1 /* Read buffer. */
+
+/* Data types modelled on sys/buf.h */
+
+/* Modelled on sys/buf.h:struct buf {}; */
+typedef buf_t {
+ bool b_iodone_flag; /* Internal - flags biodone() */
+ int b_error; /* b: errno value. */
+ int b_blkno; /* b: physical block number (volume relative) */
+ int b_resid; /* b: remaining I/O. */
+ int b_flags; /* b: B_* flags */
+ int b_bcount; /* b: valid bytes in buffer */
+ int b_data; /* b: fs private data */
+};
+
+/* XXX: auto sync/extract with md.h ? */
+#define MD_UNCONFIGURED 0
+#define MD_KMEM_FIXED 1
+#define MD_KMEM_ALLOCATED 2
+#define MD_UMEM_SERVER 3
+
+/* Device state.
+ * See: init() below;
+ * XXX: dynamic instantiation ?
+ */
+bit sc_lock;
+int sc_size;
+int sc_addr;
+byte sc_type;
+bool sc_dkbusy;
+
+/*
+ * XXX: These VAs are arbitrary - the vague intention is some form of
+ * range based validation. TBD.
+ */
+#define KERNVA 1024;
+
+#ifdef MEMORY_DISK_SERVER
+
+#define USERVA 1024;
+
+#define UMEM_QSIZE 5 /* Entries (arbitrary) - use judiciously - adds to statespace */
+chan sc_buflist = [UMEM_QSIZE] of { buf_t };
+
+#define bufq_put(_buflist, _bp) _buflist!_bp
+#define bufq_get(_buflist, _bp) _buflist?_bp
+
+#define copyin(_usrc, _kdst, _len) \
+ memcpy(_kdst, _usrc, _len)
+
+#define copyout(_ksrc, _udst, _len) \
+ memcpy(_udst, _ksrc, _len)
+
+#endif /* MEMORY_DISK_SERVER */
+
+/* We model the disk as a channel with read/write "instructions" */
+chan sc_dkdev = [2] of { int/*dst*/, int/*src*/, int/*len*/ };
+
+#define memcpy(_dst, _src, _len) { \
+ assert(_dst != _src); \
+ assert(_len != 0); \
+ sc_dkdev!_dst, _src, _len; \
+ sc_dkdev?_src, _dst, _len; \
+}
+
+/* Useful stubs */
+#define biodone(_buf) { \
+ assert(_buf.b_iodone_flag != true); \
+ _buf.b_iodone_flag = true; \
+}
+
+#define disk_busy() { sc_dkbusy = true }
+#define disk_unbusy() { sc_dkbusy = false }
+
+/* XXX: Move these into a set of library includes ? */
+/* Note: CAS implemented in an atomic {} block */
+#define mutex_enter(_mutex) \
+ atomic { \
+ (_mutex == 0) -> _mutex = 1; \
+ }
+
+#define mutex_exit(_mutex) \
+ atomic { \
+ assert(_mutex == 1); \
+ (_mutex == 1) -> _mutex = 0; \
+ }
+
+/* From sys/param.h */
+#define DEV_BSHIFT 9 /* log2(DEV_BSIZE) */
+
+/* From sys/errno.h */
+#define EIO 5 /* Input/output error */
+
+/* Other global state */
+int bytesread;
+int byteswritten;
+
+#define NPROCS 5 /*
+ * Should be less than MDDISKSIZE/1024, see bcount,
+ * blkno etc. calculations below.
+ * pid is limited to max 255, including driver code in init()
+ * thus 254 available pids
+ */
+#define MDDISKSIZE 1024 * 1024 /* 1MB */
+
+/* Drive the procs */
+init {
+ buf_t buffer;
+
+ /* XXX: Use system init routines. */
+ /* Initialise Device params */
+ sc_type = MD_KMEM_FIXED;
+ sc_size = MDDISKSIZE; /* In bytes */
+ sc_addr = KERNVA; /* Random non-zero "Kernel" address - we do not
+ do data path validation */
+
+
+ pid proc;
+
+ /* Test kernel vmem backed implementation first */
+ atomic {
+ proc = 0;
+ do
+ :: proc < NPROCS ->
+ /* Use all code-paths */
+ /* Even procs read, odd ones write */
+ buffer.b_flags = (buffer.b_flags |((proc%2) -> B_READ : B_WRITE));
+
+ /* Create some variation in buffer sizes
+ *
+ * Note: The objective here is not to
+ * unit test - rather it is to exercise
+ * code paths in various process instantiations,
+ * and to verify their mutual interaction.
+ */
+ buffer.b_bcount = (MDDISKSIZE * (proc + 1)) / (NPROCS);
+
+ /*
+ * Block number offset within device
+ */
+ buffer.b_blkno = ((buffer.b_bcount) >> DEV_BSHIFT);
+
+ run p_mdstrategy(buffer);
+ proc++
+ :: proc >= NPROCS ->
+ break
+ od
+ }
+
+#ifdef MEMORY_DISK_SERVER
+
+ /* To reset or not, that is the non-question! */
+ bytesread = 0;
+ byteswritten = 0;
+
+
+ /*
+ * Next we test the user memory server backed implementation.
+ * Here, we have to fire up a single backing server process
+ * (we assume just a single instance of the driver) which
+ * will serve the requested memory block ops on behalf of the
+ * requester processes.
+ */
+
+ sc_type = MD_UMEM_SERVER;
+ sc_addr = USERVA; /* Random non-zero "User" address - we do not
+ do data path validation */
+
+
+ run p_md_server_loop();
+
+ atomic {
+ proc = 0;
+ do
+ :: proc < NPROCS ->
+ /* Use all code-paths */
+ /* Even procs read, odd ones write */
+ buffer.b_flags = (buffer.b_flags |((proc%2) -> B_READ : B_WRITE));
+
+ /* Create some variation in buffer sizes
+ *
+ * Note: The objective here is not to
+ * unit test - rather it is to exercise
+ * code paths in various process instantiations,
+ * and to verify their mutual interaction.
+ */
+ buffer.b_bcount = (MDDISKSIZE * (proc + 1)) / (NPROCS);
+
+ /*
+ * Block number offset within device
+ */
+ buffer.b_blkno = ((buffer.b_bcount) >> DEV_BSHIFT);
+
+ run p_mdstrategy(buffer);
+ proc++
+ :: proc >= NPROCS ->
+ break
+ od
+ }
+#endif /* MEMORY_DISK_SERVER */
+}
+
diff -urN md.strategy.pml ./md.strategy.pml
--- md.strategy.pml 1970-01-01 05:30:00.000000000 +0530
+++ ./md.strategy.pml 2023-02-22 00:25:08.956729720 +0530
@@ -0,0 +1,179 @@
+/* $NetBSD$ */
+
+/* Spin process models for NetBSD md(4) md.c written by cherry */
+
+proctype p_mdstrategy(buf_t bp)
+{
+ bit is_read;
+ int off, xfer, addr;
+
+
+ mutex_enter(sc_lock);
+
+ if
+#ifdef MEMORY_DISK_SERVER
+ :: (sc_type == MD_UMEM_SERVER)
+ ->
+ bufq_put(sc_buflist, bp); /* Assume non-blocking */
+ /*
+ * We add the assert below to match cv_signal(9) semantics
+ * used in the implementation - ie; bufq_put() never blocks.
+ */
+ assert(nfull(sc_buflist));
+ mutex_exit(sc_lock);
+ goto done;
+#endif /* MEMORY_DISK_SERVER */
+
+ :: ( (sc_type == MD_KMEM_FIXED) ||
+ (sc_type == MD_KMEM_ALLOCATED)
+ ) ->
+
+ is_read = ((bp.b_flags & B_READ) && 1);
+
+ bp.b_resid = bp.b_bcount;
+
+ off = (bp.b_blkno << DEV_BSHIFT);
+
+ if
+ :: ( off >= sc_size ) ->
+ if
+ :: is_read -> goto EOF;
+ :: else -> goto set_eio;
+ fi
+ :: else ->
+ skip;
+ fi;
+
+ xfer = bp.b_resid;
+
+ if
+ :: (xfer > (sc_size - off)) ->
+ xfer = (sc_size - off);
+ :: else ->
+ skip;
+ fi
+
+ addr = sc_addr + off;
+
+ disk_busy();
+
+ /*
+ * We count the read/write totals as state for
+ * possible later property checks.
+ *
+ * But we otherwise fully exclude the data itself from
+ * the state of the control-plane, as data transfer
+ * function validation should perhaps be the domain of
+ * unit testing.
+ *
+ */
+
+ if
+ :: (is_read) -> memcpy(bp.b_data, addr, xfer);
+ bytesread = bytesread + xfer;
+ :: else -> memcpy(addr, bp.b_data, xfer);
+ byteswritten = byteswritten + xfer;
+ fi
+
+
+ disk_unbusy();
+
+ bp.b_resid = bp.b_resid - xfer;
+
+ :: else -> /* Fallback - don't block */
+ bp.b_resid = bp.b_bcount;
+set_eio:
+ bp.b_error = EIO;
+ fi
+
+EOF:
+
+ mutex_exit(sc_lock);
+
+ biodone(bp);
+
+done:
+}
+
+#ifdef MEMORY_DISK_SERVER
+proctype p_md_server_loop()
+{
+
+ bit is_read;
+ int off, xfer, addr, error;
+
+ buf_t bp;
+
+ do
+ :: true ->
+ /*
+ * Note: no messing around with sc_lock here unlike the
+ * implementation, which uses sc_lock + cv(9) + mutex(9)
+ * dance to simulate LWP awake + lock held semantics.
+ *
+ * XXX: Build a library of promela models for these kernel APIs.
+ */
+ bufq_get(sc_buflist, bp);
+
+
+ is_read = ((bp.b_flags & B_READ) && 1);
+
+ bp.b_resid = bp.b_bcount;
+
+ off = (bp.b_blkno << DEV_BSHIFT);
+
+ if
+ :: ( off >= sc_size ) ->
+ if
+ :: is_read ->
+ goto done;
+ :: else ->
+ error = EIO;
+ goto done;
+ fi
+ :: else ->
+ skip;
+ fi;
+
+ xfer = bp.b_resid;
+
+ if
+ :: (xfer > (sc_size - off)) ->
+ xfer = (sc_size - off);
+ :: else ->
+ skip;
+ fi
+
+ addr = sc_addr + off;
+
+ disk_busy();
+
+ if
+ :: (is_read) ->
+ copyin(addr, bp.b_data, xfer);
+ bytesread = bytesread + xfer;
+ :: else ->
+ copyout(bp.b_data, addr, xfer);
+ byteswritten = byteswritten + xfer;
+ fi
+
+ disk_unbusy();
+
+ if
+ :: (!error) ->
+ bp.b_resid = bp.b_resid - xfer;
+ :: else ->
+ skip;
+ fi
+
+done:
+ if
+ :: (error) ->
+ bp.b_resid = error;
+ :: else ->
+ skip;
+ fi
+ biodone(bp);
+ od
+}
+#endif /* MEMORY_DISK_SERVER */
diff -urN md.strategy.prop ./md.strategy.prop
--- md.strategy.prop 1970-01-01 05:30:00.000000000 +0530
+++ ./md.strategy.prop 2023-02-19 21:43:45.633184892 +0530
@@ -0,0 +1,13 @@
+/* $NetBSD$ */
+
+ltl
+{
+ /* We only access the disk if sc_lock is held */
+ always ((sc_dkbusy == true) implies (sc_lock == 1)) &&
+ /* memcpy() is synchronous! */
+ always (len(sc_dkdev) <= 1) &&
+ /* Eventually all disk activity should die down */
+ eventually always (len(sc_dkdev) == 0) &&
+ /* Liveness - all thread finally end */
+ eventually always (_nr_pr == 1)
+}
diff -urN md.strategy.prx ./md.strategy.prx
--- md.strategy.prx 1970-01-01 05:30:00.000000000 +0530
+++ ./md.strategy.prx 2023-02-22 00:54:27.913876007 +0530
@@ -0,0 +1,142 @@
+// Spin model extractor harness written by cherry
+//
+%F md.c
+%X -n mdstrategy
+%H
+// Disable effects of all included files and try to implement a subset of the APIs they provide.
+#define _SYS_CDEFS_H_
+#define __KERNEL_RCSID(_ign, ign)
+#define _SYS_PARAM_H_
+#define _SYS_KERNEL_H_
+#define _SYS_KMEM_H_
+#define _SYS_SYSTM_H_
+#define _SYS_BUF_H_
+#define _SYS_DEVICE_H_
+#define _SYS_DISK_H_
+#define _SYS_STAT_H_
+#define _SYS_PROC_H_
+#define _SYS_CONF_H_
+#define _UVM_UVM_EXTERN_H_
+
+
+// dev/md.h
+#define MD_UNCONFIGURED 0
+#define MD_KMEM_FIXED 1
+#define MD_KMEM_ALLOCATED 2
+
+// sys/buf.h
+#define B_READ 0x00100000 /* Read buffer. */
+#define B_WRITE 0x00000000 /* Write buffer (pseudo flag). */
+
+// sys/param.h
+#define DEV_BSHIFT 9
+
+// sys/errno.h
+#define EIO 5 /* Input/output error */
+#define ENXIO 6 /* Device not configured */
+
+// sys/null.h
+#define NULL 0
+
+#define true 1
+#define false 0
+
+struct buf {
+ int b_error;
+ int b_blkno;
+ int b_resid;
+ int b_flags;
+ int b_bcount;
+ int b_data;
+ int b_iodone_flag;
+};
+
+struct md_conf {
+ int md_type;
+ int md_size;
+ int md_addr;
+}
+
+#define MEMORY_DISK_SERVER 1
+typedef int size_t;
+typedef int bool;
+
+struct md_softc md_sc;
+#define device_lookup_private(_ign1, _ign2) (&md_sc)
+
+// The following are unused (yet) for modelling.
+#define kcondvar_t int
+#define kmutex_t int
+#define device_t int
+#define size_t int
+
+
+void md_bdevsw;
+void md_cdevsw;
+
+struct dkdriver {
+ void *dummy; /* Placeholder */
+};
+struct disk {
+ void *dummy;
+};
+
+struct dkdriver mddkdriver; /* Redundant placeholder */
+
+/* Some stubs are referred to in function prototypes */
+typedef void dev_t;
+typedef unsigned long u_long;
+typedef void cfdata_t;
+typedef void vaddr_t;
+typedef void vsize_t;
+
+#define CFATTACH_DECL3_NEW(_ign1, _ign2, _ign3, _ign4, _ign5, _ign6, _ign7, _ign8, _ign9)
+
+//XXX: MEMORY_DISK_SERVER
+#define bufq_put(_ign1, _ign2)
+#define cv_signal(_ign1)
+
+%%
+%C // c_code {}
+%%
+//%D // c_cdecl {}
+//%%
+%L
+// Modelled functions.
+// mutex(9)
+mutex_enter(... mutex_enter(sc_lock)
+mutex_exit(... mutex_exit(sc_lock)
+
+// memcpy(9)
+memcpy(addr... memcpy(addr, bufferp.b_data, xfer)
+memcpy(bp... memcpy(bufferp.b_data, addr, xfer)
+
+// disk(9)
+disk_busy(... disk_busy()
+disk_unbusy(... disk_unbusy()
+
+// bufferio(9)
+biodone(bp) biodone(bufferp)
+
+//Declare hidden sc mdstrategy
+Declare int addr mdstrategy
+Declare int off mdstrategy
+Declare int xfer mdstrategy
+Declare bit is_read mdstrategy
+%%
+
+%P
+proctype p_mdstrategy(buf_t bufferp)
+{
+ c_code { struct buf buf1;
+ buf1.b_flags |= (Pp_mdstrategy->bufferp.b_flags& B_READ) ? B_READ : B_WRITE;
+ buf1.b_bcount = Pp_mdstrategy->bufferp.b_bcount;
+ buf1.b_blkno = Pp_mdstrategy->bufferp.b_blkno;
+ Pp_mdstrategy->bp = &buf1;
+ }
+
+
+#include "_modex_mdstrategy.pml"
+
+}
+%%
\ No newline at end of file



--
Posted automagically by a mail2news gateway at muc.de e.V.
Please direct questions, flames, donations, etc. to news-***@muc.de

[Alexander Leidinger]

Post by Mathew, Cherry G.*
4) Print trace from debug trail: make spin-trace

(207) ***@ttypts/1 # make spin-trace
spin -t spinmodel.pml -p -g # -p (statements) -g (globals) -l (locals)
-s (send) -r (recv)
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5))
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) &&
((len(B2.item_list)<=5))))) && (<> ((p>0)))
Never claim moves to line 5 [(!((p>0)))]
Never claim moves to line 15 [(!((p>0)))]
<<<<<START OF CYCLE>>>>>
spin: trail ends after 272 steps
#processes: 0
queue 2 (item_list):
queue 4 (item_list):
queue 1 (item_list): [1]
queue 3 (item_list): [5][4][3][2]
_x[0].iid = 0
_x[0].cached = 0
_x[1].iid = 1
_x[1].cached = 0
_x[2].iid = 2
_x[2].cached = 0
_x[3].iid = 3
_x[3].cached = 0
_x[4].iid = 4
_x[4].cached = 0
_x[5].iid = 5
_x[5].cached = 0
_x_iid = 6
_item_rep = 5
LRUitem.iid = 0
LRUitem.cached = 0
d1 = 0
d2 = 0
p = 0
sc_lock = 0
272: proc - (ltl_0:1) _spin_nvr.tmp:14 (state 22)
16 processes created
./pan -r spinmodel.pml.trail -g
MSC: ~G 3
1: proc 0 (ltl_0) spinmodel.pml:3 (state 12) [(!((p>0)))]
2: proc 1 (:init:) spinmodel.pml:79 (state 21) [x_iid = 0]
3: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
4: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
5: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
6: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
7: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
8: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
9: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
10: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
11: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
12: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
13: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
14: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
15: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
16: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
17: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
18: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
19: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
20: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
21: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
22: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
23: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
24: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
25: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
26: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
27: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
28: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
29: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
30: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
31: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
32: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
33: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
34: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
35: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
36: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
37: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
38: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
39: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
40: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
41: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
42: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
43: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
44: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
45: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
46: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
47: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
48: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
49: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
50: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
51: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
52: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
53: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid<6))]
54: proc 1 (:init:) spinmodel.pml:82 (state 5) [D_STEP82]
55: proc 1 (:init:) spinmodel.pml:83 (state 6) [item_rep = 0]
56: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
57: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
58: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
59: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
60: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
61: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
62: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
63: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
64: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
65: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
66: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
67: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
68: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep<(x_iid%6)))]
69: proc 1 (:init:) spinmodel.pml:86 (state 8) [(run
p_arc(x[x_iid].iid,x[x_iid].cached))]
70: proc 1 (:init:) spinmodel.pml:87 (state 9) [item_rep =
(item_rep+1)]
71: proc 1 (:init:) spinmodel.pml:85 (state 12)
[((item_rep>=(x_iid%6)))]
72: proc 1 (:init:) spinmodel.pml:81 (state 18) [((x_iid>=6))]
73: proc 1 (:init:) spinmodel.pml:80 (state 20) [break]
MSC: ~G 15
74: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
75: proc 16 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
76: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
77: proc 16 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
78: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
79: proc 16 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
80: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
81: proc 16 (p_arc) spinmodel.pml:263 (state 120) [else]
82: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
83: proc 16 (p_arc) spinmodel.pml:282 (state 119) [(1)]
84: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
85: proc 16 (p_arc) spinmodel.pml:286 (state 125) [values: 3!5]
85: proc 16 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
86: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
87: proc 16 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
88: proc 16 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
89: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
90: proc 16 (p_arc) -:0 (state 0) [-end-]
91: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
92: proc 15 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
93: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
94: proc 15 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
95: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
96: proc 15 (p_arc) spinmodel.pml:194 (state 7) [values: 4!5]
96: proc 15 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
97: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
98: proc 15 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
99: proc 15 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
100: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
101: proc 15 (p_arc) -:0 (state 0) [-end-]
102: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
103: proc 14 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
104: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
105: proc 14 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
106: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
107: proc 14 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
107: proc 14 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
108: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
109: proc 14 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
110: proc 14 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
111: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
112: proc 14 (p_arc) -:0 (state 0) [-end-]
113: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
114: proc 13 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
115: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
116: proc 13 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
117: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
118: proc 13 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
118: proc 13 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
119: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
120: proc 13 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
121: proc 13 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
122: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
123: proc 13 (p_arc) -:0 (state 0) [-end-]
124: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
125: proc 12 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
126: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
127: proc 12 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
128: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
129: proc 12 (p_arc) spinmodel.pml:201 (state 11) [values: 4!5]
129: proc 12 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
130: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
131: proc 12 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
132: proc 12 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
133: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
134: proc 12 (p_arc) -:0 (state 0) [-end-]
135: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
136: proc 11 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
137: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
138: proc 11 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
139: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
140: proc 11 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
141: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
142: proc 11 (p_arc) spinmodel.pml:263 (state 120) [else]
143: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
144: proc 11 (p_arc) spinmodel.pml:282 (state 119) [(1)]
145: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
146: proc 11 (p_arc) spinmodel.pml:286 (state 125) [values: 3!4]
146: proc 11 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
147: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
148: proc 11 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
149: proc 11 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
150: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
151: proc 11 (p_arc) -:0 (state 0) [-end-]
152: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
153: proc 10 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
154: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
155: proc 10 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
156: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
157: proc 10 (p_arc) spinmodel.pml:194 (state 7) [values: 4!4]
157: proc 10 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
158: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
159: proc 10 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
160: proc 10 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
161: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
162: proc 10 (p_arc) -:0 (state 0) [-end-]
163: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
164: proc 9 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
165: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
166: proc 9 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
167: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
168: proc 9 (p_arc) spinmodel.pml:201 (state 11) [values: 4!4]
168: proc 9 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
169: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
170: proc 9 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
171: proc 9 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
172: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
173: proc 9 (p_arc) -:0 (state 0) [-end-]
174: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
175: proc 8 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
176: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
177: proc 8 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
178: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
179: proc 8 (p_arc) spinmodel.pml:201 (state 11) [values: 4!4]
179: proc 8 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
180: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
181: proc 8 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
182: proc 8 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
183: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
184: proc 8 (p_arc) -:0 (state 0) [-end-]
185: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
186: proc 7 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
187: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
188: proc 7 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
189: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
190: proc 7 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
191: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
192: proc 7 (p_arc) spinmodel.pml:263 (state 120) [else]
193: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
194: proc 7 (p_arc) spinmodel.pml:282 (state 119) [(1)]
195: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
196: proc 7 (p_arc) spinmodel.pml:286 (state 125) [values: 3!3]
196: proc 7 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
197: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
198: proc 7 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
199: proc 7 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
200: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
201: proc 7 (p_arc) -:0 (state 0) [-end-]
202: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
203: proc 6 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
204: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
205: proc 6 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
206: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
207: proc 6 (p_arc) spinmodel.pml:194 (state 7) [values: 4!3]
207: proc 6 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
208: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
209: proc 6 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
210: proc 6 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
211: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
212: proc 6 (p_arc) -:0 (state 0) [-end-]
213: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
214: proc 5 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
215: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
216: proc 5 (p_arc) spinmodel.pml:192 (state 126)
[(T2.item_list??[eval(x_t.iid)])]
217: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
218: proc 5 (p_arc) spinmodel.pml:201 (state 11) [values: 4!3]
218: proc 5 (p_arc) spinmodel.pml:201 (state 11) [D_STEP201]
219: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
220: proc 5 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
221: proc 5 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
222: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
223: proc 5 (p_arc) -:0 (state 0) [-end-]
224: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
225: proc 4 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
226: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
227: proc 4 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
228: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
229: proc 4 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
230: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
231: proc 4 (p_arc) spinmodel.pml:263 (state 120) [else]
232: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
233: proc 4 (p_arc) spinmodel.pml:282 (state 119) [(1)]
234: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
235: proc 4 (p_arc) spinmodel.pml:286 (state 125) [values: 3!2]
235: proc 4 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
236: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
237: proc 4 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
238: proc 4 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
239: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
240: proc 4 (p_arc) -:0 (state 0) [-end-]
241: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
242: proc 3 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
243: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
244: proc 3 (p_arc) spinmodel.pml:192 (state 126)
[(T1.item_list??[eval(x_t.iid)])]
245: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
246: proc 3 (p_arc) spinmodel.pml:194 (state 7) [values: 4!2]
246: proc 3 (p_arc) spinmodel.pml:194 (state 7) [D_STEP194]
247: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
248: proc 3 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
249: proc 3 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
250: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
251: proc 3 (p_arc) -:0 (state 0) [-end-]
252: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
253: proc 2 (p_arc) spinmodel.pml:188 (state 3) [((sc_lock==0))]
254: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
255: proc 2 (p_arc) spinmodel.pml:192 (state 126)
[(!((((T1.item_list??[eval(x_t.iid)]||B1.item_list??[eval(x_t.iid)])||T2.item_list??[eval(x_t.iid)])||B2.item_list??[eval(x_t.iid)])))]
256: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
257: proc 2 (p_arc) spinmodel.pml:237 (state 122)
[(((len(T1.item_list)+len(B1.item_list))<5))]
258: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
259: proc 2 (p_arc) spinmodel.pml:263 (state 120) [else]
260: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
261: proc 2 (p_arc) spinmodel.pml:282 (state 119) [(1)]
262: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
263: proc 2 (p_arc) spinmodel.pml:286 (state 125) [values: 3!1]
263: proc 2 (p_arc) spinmodel.pml:286 (state 125)
[T1.item_list!x_t.iid]
264: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
265: proc 2 (p_arc) spinmodel.pml:289 (state 131)
[assert((sc_lock==1))]
266: proc 2 (p_arc) spinmodel.pml:289 (state 129) [((sc_lock==1))]
267: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
268: proc 2 (p_arc) -:0 (state 0) [-end-]
269: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
270: proc 1 (:init:) -:0 (state 0) [-end-]
<<<<<START OF CYCLE>>>>>
271: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
272: proc 0 (ltl_0) spinmodel.pml:15 (state 22) [(!((p>0)))]
spin: trail ends after 272 steps
#processes 1:
272: proc 0 (ltl_0) spinmodel.pml:15 (state 22) (invalid end state)
(!((p>0)))
global vars:
(struct B1)
chan item_list (=1): len 0:
(struct B2)
chan item_list (=2): len 0:
(struct T1)
chan item_list (=3): len 1: [1,],
(struct T2)
chan item_list (=4): len 4: [5,], [4,], [3,], [2,],
byte p: 0
bit sc_lock: 0


Bye,
Alexander.

[Mathew, Cherry G.*]

[...]

Post by Alexander Leidinger
spinmodel.pml:80, state 28, "D_STEP80"
spinmodel.pml:80, state 53, "D_STEP80"
spinmodel.pml:154, state 70, "B1.item_list?_"
spinmodel.pml:80, state 79, "D_STEP80"
spinmodel.pml:90, state 85, "D_STEP90"
spinmodel.pml:78, state 86,
(((len(T1.item_list)!=0)&&((len(T1.item_list)>p)||(B2.item_list??[eval(x[x_iid].iid)]&&(len(T1.item_list)==p)))))"
spinmodel.pml:78, state 86, "else"
spinmodel.pml:73, state 88, "D_STEP73"
spinmodel.pml:159, state 90, "assert((len(B1.item_list)==0))"
spinmodel.pml:160, state 94, "D_STEP160"
spinmodel.pml:152, state 95, "((len(T1.item_list)<64))"
spinmodel.pml:152, state 95, "else"
spinmodel.pml:183, state 100, "B2.item_list?_"
spinmodel.pml:198, state 128, "(1)"
spinmodel.pml:268, state 155, "-end-"
(13 of 155 states)

[...]

These correspond to "Case A" in arc.pml, which were never entered
because the driver file wasn't able to create the right sequence to
exercise those code paths. I'll look at this later - as this is an
illustrative project, it may even make sense to just find an input
"trace" as an input array that is guaranteed to make the state machine
enter all paths.

Thanks for the confirmation trace!

[Adriaan de Groot]

For what it's worth, spin is available from ports (devel/spin), which I've
just adopted and updated to 6.5.2, so it is quite straightforward to get this
running on any recent FreeBSD system.

I tested only with the ancient Peterson's mutual exclusion, which resolves
instantly. Mailing-list archives don't preserve attachments, so, Cherry, if
you could send it me directly that would be lovely. I spotted A. Mader's PLC
Controller in the SPIN documents, that is one I am familiar with, and then
realised that academic papers from the 2000s don't come with source code :(

[ade]

[Baptiste Daroussin]

Post by Adriaan de Groot
For what it's worth, spin is available from ports (devel/spin), which I've
just adopted and updated to 6.5.2, so it is quite straightforward to get this
running on any recent FreeBSD system.
I tested only with the ancient Peterson's mutual exclusion, which resolves
instantly. Mailing-list archives don't preserve attachments, so, Cherry, if
you could send it me directly that would be lovely. I spotted A. Mader's PLC
Controller in the SPIN documents, that is one I am familiar with, and then
realised that academic papers from the 2000s don't come with source code :(

Wrong mailing list do preserve attachemnts, since we migrated out of mailman, we
stopped alterring emails if a mail is distributed via the mailing list then its
integrity is preserved, if you want to get the full email later on, then you can
always fallback on the .txt archive which is actually the mail in a mbox format
meaning readable by any sane Mail User Agent.

For example for this email:
https://lists.freebsd.org/archives/freebsd-hackers/2023-September/002488.txt

Bapt


--
Posted automagically by a mail2news gateway at muc.de e.V.
Please direct questions, flames, donations, etc. to news-***@muc.de

[Alexander Leidinger]

Post by Mathew, Cherry G.*
Hi Alexander,
[...]
AL> How long is this supposed to take? For me it took about 2
AL> seconds to finish.
Apologies, I should have given more detailed instructions.
1) Generate the model from spec: make spin-gen
2) Build the model: make spin-build
3) Run the model: make spin-run
This is the heavy duty part, which takes up quite a bit of vmem (my
process dies at about 8GB due to lack of swap etc. - makes no sense to
thrash it beyond that without RAM - it slows down a lot).
If all goes well with step 3) , then you will see a summary of the run
on console. However, if there was an inconsistency or error detected in
the run, then a tracefile is generated (spinmodel.pml.trail). I've
included a target to dump a human friendly version of this trace.

And just when I've send the mail, it finished... :)
---snip---
Samstag, 02. September 2023, 18:51:21
(203) ***@ttypts/1 # time make spin-gen
cp arc.pml model #mimic modex
cat arc.drv > spinmodel.pml;cat model >> spinmodel.pml;cat arc.inv >>
spinmodel.pml;
spin -a spinmodel.pml
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5))
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) &&
((len(B2.item_list)<=5))))) && (<> ((p>0)))
make spin-gen 0,04s user 0,11s system 24% cpu 0,585 total

Samstag, 02. September 2023, 18:51:29
(204) ***@ttypts/1 # time make spin-build
cc -o pan pan.c
make spin-build 0,47s user 0,26s system 56% cpu 1,286 total

Samstag, 02. September 2023, 18:51:37
(205) ***@ttypts/1 # time make spin-run
cc -o pan pan.c
./pan -a #Generate arc.pml.trail on error
Depth= 271 States= 1e+06 Transitions= 2.04e+06 Memory= 194.550
t= 4.47 R= 2e+05
Depth= 271 States= 2e+06 Transitions= 4.09e+06 Memory= 264.081
t= 9.16 R= 2e+05
Depth= 271 States= 3e+06 Transitions= 6.16e+06 Memory= 334.101
t= 13.5 R= 2e+05
Depth= 271 States= 4e+06 Transitions= 8.25e+06 Memory= 410.370
t= 18.4 R= 2e+05
Depth= 271 States= 5e+06 Transitions= 1.04e+07 Memory= 485.272
t= 23.4 R= 2e+05
Depth= 271 States= 6e+06 Transitions= 1.25e+07 Memory= 560.175
t= 28 R= 2e+05
Depth= 271 States= 7e+06 Transitions= 1.46e+07 Memory= 635.077
t= 33.1 R= 2e+05
Depth= 271 States= 8e+06 Transitions= 1.67e+07 Memory= 710.077
t= 38 R= 2e+05
Depth= 271 States= 9e+06 Transitions= 1.88e+07 Memory= 787.812
t= 43.2 R= 2e+05
Depth= 271 States= 1e+07 Transitions= 2.09e+07 Memory= 867.987
t= 48.5 R= 2e+05
Depth= 271 States= 1.1e+07 Transitions= 2.3e+07 Memory= 948.163
t= 53.5 R= 2e+05
Depth= 271 States= 1.2e+07 Transitions= 2.51e+07 Memory= 1028.339
t= 58.7 R= 2e+05
Depth= 271 States= 1.3e+07 Transitions= 2.72e+07 Memory= 1108.515
t= 63.8 R= 2e+05
Depth= 271 States= 1.4e+07 Transitions= 2.93e+07 Memory= 1188.202
t= 69.1 R= 2e+05
Depth= 271 States= 1.5e+07 Transitions= 3.15e+07 Memory= 1267.401
t= 74.5 R= 2e+05
Depth= 271 States= 1.6e+07 Transitions= 3.36e+07 Memory= 1346.503
t= 79.9 R= 2e+05
Depth= 271 States= 1.7e+07 Transitions= 3.58e+07 Memory= 1425.605
t= 85.2 R= 2e+05
[...]
Depth= 271 States= 2.07e+08 Transitions= 4.44e+08 Memory= 20175.351
t= 1.22e+03 R= 2e+05
Depth= 271 States= 2.08e+08 Transitions= 4.46e+08 Memory= 20262.558
t= 1.22e+03 R= 2e+05
Depth= 271 States= 2.09e+08 Transitions= 4.49e+08 Memory= 20349.667
t= 1.23e+03 R= 2e+05
pan:1: acceptance cycle (at depth 270)
pan: wrote spinmodel.pml.trail

(Spin Version 6.5.0 -- 1 July 2019)
Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 184 byte, depth reached 271, errors: 1
1.0465042e+08 states, stored (2.09301e+08 visited)
2.4007432e+08 states, matched
4.4937506e+08 transitions (= visited+matched)
44667618 atomic steps
hash conflicts: 63844226 (resolved)

Stats on memory usage (in Megabytes):
21158.112 equivalent memory usage for states (stored*(State-vector
+ overhead))
18344.457 actual memory usage for states (compression: 86.70%)
state-vector as stored = 156 byte + 28 byte overhead
2048.000 memory used for hash table (-w28)
0.534 memory used for DFS stack (-m10000)
17.170 memory lost to fragmentation
20375.839 total actual memory usage



pan: elapsed time 1.23e+03 seconds
pan: rate 169922.52 states/second
make spin-run 1199,05s user 34,46s system 99% cpu 20:33,94 total
---snip---

Hope this helps,
Alexander.

[Dag-Erling Smørgrav]

Post by Mathew, Cherry G.*
I'm hoping that someone can help me complete the current run, as I don't
have the computing resources required to run the full model (about 16GB
RAM).

16 GB is not a huge amount of memory. Would it help if you had access
to a jail or VM with enough memory to run the model yourself?

DES

[Mathew, Cherry G.*]

Post by Dag-Erling Smørgrav

Post by Mathew, Cherry G.*
I'm hoping that someone can help me complete the current run, as
I don't have the computing resources required to run the full
model (about 16GB RAM).

16 GB is not a huge amount of memory. Would it help if you had
access to a jail or VM with enough memory to run the model
yourself?

Hi DES,

You probably caught up on the rest of the thread - I figured out a way
to reduce the state space explosion (it's got to do with how
spin/promela semantics map to regular function style languages) - in the
end, it all came down to just around a second runtime. I think the
complexity will remain there, until I improve it for
re-entrancy/concurrency/multi-threaded use.

(currently the code/model assumes no re-entry).

I will fall back on your offer if it becomes unmanageable then.

Many Thanks,