Verification of the Distributed Hybrid Cache Coherence protocol of the TeraScale Architecture
This repository contains formal models of the DHCCP protocol used in TSAR.
These models were built by students at Sorbonne Université (formerly Université Pierre et Marie Curie), at the Laboratoire d'Informatique de Paris 6 (LIP6), in Paris, France.
Students that participated :
- Mohamad Najem, Master 1, 2011
- Akli Mansour, Master 1, 2012
- Zahia Gharbi, Master 1, 2013
- Di Zhao, Master 2, 2015
Each of these students built models and a report (in French) on their work, which can be found in the "Reports" folder. There are also a couple of slide shows and other documentation (automata of the components) in that folder.
These students were supervised by Emmanuelle Encrenaz, Quentin Meunier and Yann Thierry-Mieg, all three being professors at Sorbonne Université. See each report for more details.
Three modeling languages were used to build the models
- Promela the language of the tool Spin
- Divine Language the language of the tool DiViNe. We used Divine version 2 in these experiments.
- GAL the Guarded Action Language of the ITS-tools
There is a folder with a README for each of these languages, containing the models and how to run the experiments.
This repository is a companion to our MARS2018 paper.
All model files in this repository can be freely used and modified. The various reports remain the copyrighted property of their respective authors, they may be copied and distributed but not edited.
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.