-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://www.inrialpes.fr/vasy/cadp
-- This software is subject to copyright restrictions defined in 
-- the document "Contrat de mise a` disposition de logiciels"

[Last updated: Mon Aug 12 10:33:47 CEST 2024]

This directory contains an example that presents the formal analysis
(verification and performance evaluation) of mutual exclusion protocols,
specified in LNT, for N concurrent processes interacting by shared variables
[Mateescu-Serwe-13].

The whole analysis evaluation scenario for N processes (N in {2, 3, 4, 5})
is described and commented in the file "demo.svl".

For N == 2, it can be executed by typing
$	svl demo
or even simply
$	svl

The analysis scenario for N processes and a given list L of protocols can be
executed by typing
$	svl demo N L
where L is a white-space-separated list of protocols (i.e., names of files
in directory Protocols, but without extension ".lnt").

After execution of the SVL scenario, all generated files can be removed by 
typing
$	svl -clean demo
or even simply
$	svl -clean

In the naming of files, ${N}, ${M}, and ${K} are numeric values, ${N} being
the number of processes trying to access the critical section, and ${M}
and ${K} being the parameters used in the automatic generation of mutual
exclusion protocols in [BarDavid-Taubenfeld-03].

   demo.svl			SVL script (state space generation & analysis)
   mutex.plot			Gnuplot script (diagram generation)

Directory Protocols contains the models of the mutual exclusion protocols:

   anderson.lnt			Anderson's array-based protocol
   burns_lynch.lnt		Burns & Lynch's protocol
   bw_bakery.lnt		Black-White Bakery protocol
   clh.lnt			Craig and Landin & Hagersten's protocol
   dekker.lnt			Dekker's protocol
   dijkstra.lnt			Dijkstra's protocol
   kessels_2.lnt		Kessels's protocol for two processes
   knuth.lnt			Knuth's protocol for n processes
   knuth_2.lnt			Knuth's protocol for two processes
   lamport.lnt			Lamport's protocol
   mcs.lnt			Mellor-Crummey & Scott's protocol
   peterson.lnt			Peterson's protocol for n processes
   peterson_2.lnt		Peterson's protocol for two processes
   peterson_tree.lnt		generalisation of Peterson's protocol using a
				binary tree of locks
   szymanski.lnt		Szymanski's protocol
   tas.lnt			test-and-set protocol
   ttas.lnt			test--test-and-set protocol
   trivial.lnt			trivial one-bit protocol
   mutex_${M}b_p${K}.lnt	generated protocol [BarDavid-Taubenfeld-03]
   mutex_${M}b_c_p${K}.lnt	generated protocol [BarDavid-Taubenfeld-03]
   mutex_${M}b_c_p${K}_orig.lnt	generated protocol [BarDavid-Taubenfeld-03]

Directory Components contains processes modeling components that are
independent from the number of processes competing for access to the critical
section:

   CHANNELS.lnt			channel definitions
   EXTENDED_VARIABLE_ARRAY.lnt	model of an array of shared variables
   FUNCTIONS.lnt		function definitions
   MEMORY.lnt			process modeling a shared memory (for CLH)
   MESI_CACHE.lnt		coherent cache using the MESI cache protocol
   QUEUE.lnt			process modeling a shared queue
   TUPLE_ARRAY.lnt		model of an array of tuples (for BW bakery)
   TYPES_COMMON.lnt		data type definitions
   VARIABLE.lnt			model of a shared variable
   VARIABLE_ARRAY.lnt		model of an array of shared variables

Directory Architectures contains instantiations of the overall architecture
for various numbers of variables and processes, according to the following
naming scheme:

   ARCH_${M}B_${N}.lnt		architecture with ${M} variables
   ARCH_${M}B_A_${N}.lnt	architecture with ${M} variable array
   ARCH_${M}B_Q_${N}.lnt	architecture with ${M} variables and a queue
   ARCH_TREE_${N}.lnt		architecture with a tree of binary protocols
   TYPES_${N}.lnt		data type definitions

Currently, only the LNT modules for N in {2, 3, 4, 5} are provided. For
larger values of N, the directory Architectures could be extended with
further modules written according to the existing ones.


References:

[Anderson-Kim-Herman-03]
   J.H. Anderson, Y.-J. Kim, and T. Herman.
   Shared-memory Mutual Exclusion: Major Research Trends since 1986.
   Distributed Computing 16(2-3):75-110, 2003.

[BarDavid-Taubenfeld-03]
   Automatic Discovery of Mutual Exclusion Algorithms.
   Yoah Bar-David and Gadi Taubenfeld.
   Proceedings of the 17th International Conference on Distributed Computing,
   Lecture Notes in Computer Science 2848, pages 136-150, October 2003.

[David-Guerraoui-Trigonakis-13]
   Everything You Always Wanted to Know About Synchronization but Where
   Afraid to Ask.
   Tudor David, Rachid Guerraoui, and Vasileios Trigonakis.
   Proceedings of the 24th ACM SIGOPS Symposium on Operating Systems
   Principles, pages 33-48, November 2013.

[Mateescu-Serwe-13]
   Model Checking and Performance Evaluation with CADP Illustrated on
   Shared-Memory Mutual Exclusion Protocols.
   Radu Mateescu and Wendelin Serwe.
   Science of Computer Programming 78(7):843-861, 2013.
   http://cadp.inria.fr/publications/Mateescu-Serwe-13.html

[Yang-Anderson-95]
   J.-H. Yang and J. H. Anderson.
   A Fast, Scalable Mutual Exclusion Algorithm.
   Distributed Computing 9(1):51-60, 1995.

For a complete list of references for the different protocols, please refer
to [Mateescu-Serwe-13].