Re: ARC model specified in spinroot/promela

["Mathew\, Cherry G.*" <c%bow.st@localhost>]

>>>>> Mathew, Cherry G * <c%bow.st@localhost> writes:

[...]

    > 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.

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
+# <c%bow.st@localhost> 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 *~