Concurrent Protocol Verification with PRISM
What I did
I modeled mutual-exclusion protocols in PRISM and examined safety, progress, waiting rewards, and deliberately faulty variants.
CS490 supervised capstone · September 2026–present
My contribution
Concurrent-protocol modeling and verification within a capstone team
- Built and investigated PRISM models of concurrent mutual-exclusion protocols.
- Exported Dekker results and documented models, properties, and graphs in LaTeX.
- Extended the work to Peterson comparisons, counterexamples, and Bakery models.
Outcome
Verified properties of two 5,738-state Bakery models and exposed a mutual-exclusion failure in a faulty variant.
My part of the capstone
This is a faculty-supervised team project on probabilistic model checking. My branch of the work concerns concurrent programs and mutual exclusion. The team’s weekly task log assigns Thomas the Dekker graphs and LaTeX explanation, another mutual-exclusion implementation, and investigation of more interesting or faulty protocols. The models, exported results, and reports document the work that followed.
My contribution is the concurrent-protocol study, rather than every topic investigated by the team. I use PRISM to turn a program-level question into an explicit model and a property: can two processes enter the critical section together, can the system deadlock, and what completion or waiting behavior is possible under scheduling choices?
Modeling the question precisely
I investigated Dekker’s and Peterson’s two-process protocols and a three-process Lamport Bakery model. Markov decision processes represent probabilistic requests alongside nondeterministic scheduling. A request probability applies when a process is scheduled; it is not the probability that the CPU selects that process.
For waiting comparisons, I used a common request-to-entry reward definition and matched horizons. The curve below comes from the repository’s exported PRISM data. Its vertical axis measures cumulative pending-request model steps, not elapsed seconds or average delay per completed request. This distinction is essential when interpreting the curves.
A concrete verification result
The one-request-per-process Bakery abstraction has 5,738 reachable states for each of two request-probability profiles. The recorded checks gave:
| Property | Equal requests | Unequal requests |
|---|---|---|
| Maximum probability of mutual-exclusion violation | 0 | 0 |
| Maximum probability of deadlock | 0 | 0 |
| Minimum probability that all processes finish | 1 | 1 |
I also examined a variant that removes the choosing-flag wait. A process can pause before publishing its ticket while another process treats the unpublished ticket as zero. That creates a route to simultaneous entry. The faulty model has 9,772 states and a maximum violation probability of 1, meaning a violating scheduling strategy exists, not that every execution fails.
What this work taught me
Writing the property is as important as writing the model. Changing the request cycle, atomicity assumption, or reward definition can change what a result means. A sample trace explains one execution; a model-checking query reasons about the modeled state space. Neither should be described as a timing benchmark of a real multithreaded application.
Model boundaries and reproducibility
The recorded Bakery results use PRISM 4.10.1, separate ticket reads and publication, sequential interleaving, atomic individual register access, and at most one request per process. There are no crashes or recovery. The ticket bound does not justify unlimited cyclic requests, and completion results should not be generalized to older cyclic Dekker/Peterson models.
The accompanying reports explain PCTL queries, request profiles, finite-horizon experiments, and exported graphs. The deliberately broken Bakery model was checked for its safety counterexample; it should not be described as having passed the full correct-model test suite.
Code and the supporting task log are available on request: contact me. The repository remains private.