PAFAS at work: comparing the worst-case efficiency of three buffer implementations

The authors use PAFAS (Process Algebra for Faster Asynchronous Systems) to compare the worst-case efficiency of three bounded-buffer implementations: Fifo, Pipe and Buff. Fifo implements the buffer as a first-in-first-out queue, Pipe implements the buffer as a pipeline queue and Buff implements the buffer as circular queue in an array. We contrast our results with those by S. Arun-Kumar and M. Hennessy (1992) and l. Jenner and W. Vogler (1996) which also aim at comparing the three implementations of the bounded buffer according to some efficiency measure