ParaVerifier

ParaVerifier is an automatic framework for proving parameterized cache coherence protocols.

---

Background

Parameterized verification of cache coherence protocols is an important but challenging research problem. We have developed an automatic framework ParaVerifier to handle this research problem:

1. It first discovers auxiliary invariants and the corresponding causal relations between invariants and protocol rules from a small reference instance of the verified protocol;
2. The discovered invariants and causal relations can then be generalized into their parameterized form to automatically construct a formal proof to establish the correctness of the protocol.

ParaVerifier has been successfully applied to a number of benchmarks.

---

Download

Platforms

Currently supported platforms:

• Linux

Requirements

The following tools are required to run paraVerifier on your computer:

• Forte
• Z3
• NuSMV
• Isabelle

Installation

Make sure the requirements have been installed properly before trying steps below. Take the mesi protocol as an example:

1. enter the protocol directory

   $ cd mesi

2. run forte_nusmv.sh to compute reachable states:

   $ ./forte_nusmv.sh

3. run forte

   $ fl

   then load the mesi.fl file

   :load "mesi.fl";

4. use the mesi.thy script in proof assistant Isabelle. For small case study like mesi, it is feasible to directly run the proof document in Isabelle/Jedit interface. However, for modrate case like german2000 with data paths, Isabelle/Jedit will be very slow to run the proof document. Let alone the Flash protocols. Therefore, we provide a script ROOT to build the proof script in console mode. In order to check the proof, you can just run the following command in the path where the proof and scripts are in:

   $Isabelle2014/bin/isabelle - v -d . -b Main_Session

   Each proof script has been machine checked by Isabelle.

---

Experiments

We have applied ParaVerifier to a number of benchmarks:

protocol	#rule	#inv	time(s)	mem(Mb)	invs	rels	thy
MESI	4	3	0.68	11.5	mesi_inv	mesi_rel	mesi.zip
MOESI	5	3	0.65	23.2	moesi_inv	moesi_rel	moesi.zip
German-ish	6	3	2.39	23.0	germanIsh_inv	germanIsh_rel	germanIsh.zip
German	13	24	4.09	26.7	german_inv	german_rel	german.zip
German-data	15	50	45.71	29.4	german_data_inv	german_data_rel	germanData.zip
Flash-no-data	73	112	1457.42	169.4	flash_inv	flash_rel	flash.zip

Some Notes

1. An invariant in a line of table should be read by adding a negative operator.
   For instance
   $$( ( home\_exclusive\_granted=false) \land (!( memdata=auxdata) ) )$$
   is in the first line of the invariants of the German2000Data property,
   $$NOT ( ( home\_exclusive\_granted=false) \land (!( memdata=auxdata) ) )$$
   is the actual invariant.

2. The node index 1,2, 3, and etc represents a variable i1, i2, i3, and etc respectively. These node are symmetric to each other. 0 in Flash protocol represents the Home node index. Home node is not symmetric to the others.

3. Flash protocols are too complex to be proved by only a proof because a single proof script needs 16M, which can not be dealt by Isabelle. We divide the single proof into a number of small single proofs. flashPub.thy contains the definitions of rule and invariants, and prepares the lemmas to prove the first part of proof obligation of the consistency lemma. flashiRev.thy proves that the relation invHoldForRule invi r invs holds for each rule instance r in rules N. flashiBra.thy proves that the relation invHoldForRule invi r invs holds for any r in rules N. flashMainLemma.thy proves the second part of proof obligation of the consistency lemma. At last, the flash.thy finishes the proof of the invariants.

4. After the auxiliary invariants are found, the formula set $\mathsf{pinvs}~ N$ in Table can be used to analyze and verify the design of the protocol. In fact, they gives a complete logical characterization of the semantics of the protocol. It will gives a deep insight of the protocol. These properties are divided into two categories:

   1. correspondence between control signals;
   2. mutual exclusion between control signals.

   We have do analysis on the meaning of invariants searched in the case studies of German, German200Data, and FLASH protocols. They can be lownloaded from German, German2000Data, and FLASH.

5. The algorithm of InvFinder is described in the following article:

   invFinder Algorithm

Contact Us

You can contact us by e-mail:

• lyj

---