Models for: On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them

Files for the mCRL2 models used for the verifications described in On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them by Rob van Glabbeek, Daniele Gorla and Myrthe Spronck. This record contains the following files: mCRL2 specification files: Anderson.mcrl2A model of Anderson's MUTEX algorithm.Default configuration: 2 processes and atomic registers, initialized for checking post-doorway bounded bypass with a bound of 2, with the doorway placed at the end of the second line of the algorithm. Dekker.mcrl2A model of Dekker's MUTEX algorithm.Default configuration: 2 processes and atomic registers, initialized for checking bounded bypass with bound 100. The initial value of TURN is 0. Bar-David_Lamport1bit.mcrl2A model of Bar-David's algorithm for turning any deadlock-free MUTEX algorithm into a starvation-free one, using Lamport's 1-bit MUTEX algorithm as the sub-algorithm.Default configuration: 3 processes and safe registers, initialized for checking intermittent bounded bypass with a bound of 7 for bypasses and 3 for interrupting writes. The initial value of TURN is 0. Modal mu-calculus formulas: bb.mcfModal mu-calculus formula for bounded bypass and post-doorway bounded bypass, depending on where the doorway tag is placed. ibb.mcfModel mu-calculus formula for intermittent bounded bypass, where any write may be chosen to be interrupting. ibb_thm413.mcfModal mu-calculus formula for intermittent bounded bypass where the exact set of interrupting writes is pre-defined to be those considered in Theorem 4.13 from the paper. Python scripts: runsymbolic.pyThis script checks a property for a model without generating evidence.Call "python runsymbolic.py ". runcounter.pyThis script checks a property for a model and generates evidence, often much slower than runsymbolic.py.Call "python runcounter.py ". Text files and pdfs: model_modification.txtIn-depth description of which modifications can be made to the models to check different properties, different bounds or different register types. ibb_thm.pdfPresentation and explanation of ibb_thm413.mcf, similar in style to how bb.mcf and ibb.mcf are explained in the associated paper. In order to run the python scripts, mCRL2 must be installed. Information on how to install mCRL2 can be obtained here: https://mcrl2.org/web/home/download.html. The results reported in the paper were obtained using mCRL2 version 202507.0.