# ILCMP **Repository Path**: x-jay/ILCMP ## Basic Information - **Project Name**: ILCMP - **Description**: An Increamental Approach to the CMP Method for Parameterized Verification of Cache Coherence Protocols - **Primary Language**: Python - **License**: Not specified - **Default Branch**: master - **Homepage**: None - **GVP Project**: No ## Statistics - **Stars**: 0 - **Forks**: 1 - **Created**: 2022-11-02 - **Last Updated**: 2022-11-02 ## Categories & Tags **Categories**: Uncategorized **Tags**: None ## README # ILCMP #### Introduction We implemented a framework ILCMP to automate the CMP method for parameterized verification, including find noninterference lemmas automatically which is usually done by manual analysis. Moreover, our tool murphiGen can automatically complete guard strengthening and abstraction process , then generate the abstract protocol model in a file ABSProt.m #### Workflow Firstly, we abstract the Murphi model of a parameter protocol, and then find the counterexample of this abstract protocol with the Model Checking method. For the counterexample, the auxiliary invariants are obtained automatically by association rule learning method. These invariants are combined with the original protocol to form a CMP process. Repeat the above steps until no counterexamples generate. The specific process is shown in the figure below. ![framework](/fig/framework.png) #### Requirement 1. Cmurphi 5.5.0 http://mclab.di.uniroma1.it/site/index.php/software/18-cmurphi 2. Python 3.8.12 3. Lark 1.1.2 Note that these programs runs on MAC or Linux system #### Run an Example 1. Download the program and libraries mentioned above. 2. Modify the file settings.py, set the variables MU_PATH, MU_INCLUDE, GXX_PATH, which mean path of CMurphi, path of include directory of CMurphi and path of g++ compiler respectively. MU_FILE_DIR refers to when CMurphi is called to check protocol, a directory is created under MU_FILE_DIR to hold temporary files, and you can change it to where you want. MU_CHECK_MEMORY indicates how much memory you will allocate to the CMurphi program. 3. Run the file `python murphiGen.py --task mutualEx --simp n`, in which the 'mutualEx' can be replaced to another protocol name. It will automatically perform ILCMP work until ‘success!’ is displayed on the terminal. After step 3, some files are generated under the path ./prot/. The 'prot' represents the name of protocol you want to verify. A file named ABSprot.m will appear in the path, which is the final abstract protocol. In the meantime, the information about the strengthen process and lemmas will be contained in abs_process.csv in the folder corresponding to the protocol. In addition to these, prot.txt is the reachable set of the protocol; prot.csv is also the reachable set of the protocol, except that it is represented as a CSV file; trans_dataset.csv is the extended reachable set, which gives a Boolean value for each predicate. assoRules.txt is the association rules has learned; str_prot.m retains the result of the strengthen for each rule. Because some file has existed in the path ./prot/, so you can just run `python murphiGen.py --task mutualEx` to get a quick verification using the invariant in the directory without learning. #### ABSprot.m The ABSprot.m is an abstraction of the original protocol. It contains the original and abstracted rules, as well as variable definitions, initializations, and invariants, etc. #### abs_process.csv The abs_process.csv file records the protocol strengthening information, including which rules were strengthened and which lemmas were used in the process. Notice that these processes are recorded in sequence. ![abs_process](/fig/abs_process.jpg) As shown above, flash_ctc_10_origin is strengthened in order: ‘NI_Remote_Get_Put’, ‘PI_Remote_PutX’… For ‘NI_Remote_Get_Put’, using Lemma2,Lemma1,… to strengthen it. #### str_prot.m str_prot.m contains the original rules and the rule strengthened with lemmas. #### prot.txt prot.txt is the output file of CMurphi, which is the reachable set of the protocol. #### prot.csv Prot.csv is the reachable set represented in a CSV file. As shown in the following example, mutualEx has seven states and three variables. Each line represents a reachable state and the value of the variables. ![reachable state of prot](/fig/prot.jpg) #### trans_dataset.csv Trans_dataset.csv extends variables from Prot.csv, where the first line is all variables and their possible values, also known as atomic predicates, and lines 2-8 are their Boolean values. ![The transformed dataset](/fig/trans.jpg) #### cmurphi5.5.0-v1_hid Original Murphi tool has its limitation in supporting eliminating too many invariants. - Murphi adopts the on-the-fly mode in which it will stop once an invariant is violated. - Murphi's compiler reports an error when the number of invariants exceeds about 100. Usually the default number of invarints is small, less than 500. However, the number of learning invariants can exceed 10000. - Since checking invariants also need time, Murphi will run extremely long when there are too many invariants to be checked in each reachable state. Therefore, we extend Murphi to work in a mode in which it stops until all invariants are checked to be false or all reachable states are enumerated, and the invariants which fails in model checking are listed in output. Besides, a hundred of invariants are formed as a group and subjected to model checking, which is executed in a spawn of process of executing Murphi; and all invariants are divided into groups and model checked by many processes in parallel. This multi-process approach obviously reduces the time to select auxiliary invariants. #### Result | | Node | States | Asso | aux\_invariants | States(abs) | Learning | Filter | Strengthen | Total | |:-----------:|:----:|:------:|:--------:|:---------------:|:-----------:|:--------:|:--------:|:----------:|:--------:| | moesi | 2 | 6 | 0 | 0 | 7 | 0 | 0 | 0 | 2.89 | | mesi | 2 | 5 | 0 | 0 | 5 | 0 | 0 | 0 | 2.96 | | mutualEx | 2 | 7 | 532 | 3 | 18 | 0.013 | 4.43 | 0.013 | 8.72 | | mutdata | 2 | 23 | 1464 | 8 | 46 | 0.027 | 5.6 | 0.024 | 14.21 | | german | 2 | 750 | 30010 | 7 | 1185 | 0.33 | 2.52 | 0.021 | 8.62 | | german_data | 2 | 852 | 266481 | 21 | 1314 | 2.50 | 10.56 | 0.10 | 29.91 | | flash | 2 | 32439 | 6399077 | 257 | 183596 | 141.35 | 908.43 | 1.62 | 1160.09 | | flash_data | 2 | 701624 | 12321620 | 282 | 5295934 | 3493.97 | 25438.96 | 1.94 | 29597.11 | We have verified Bus/Directory-based cache consistency protocols, including Flash protocol which is industrial-level. The CMP method of each protocol is also formally proved.