Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Index of /~pieter/cdp/ben-ari
The files in this directory are the Promela versions of the
many of the ADA programming examples from M. Ben-Ari, Principles of
Concurrent and Distributed Programming 1/e, Published April
1990 by Prentice Hall PTR, 225 pp, ISBN 13-711821-X
make.sh bash script for running spin on the various examples
ben-ari.tar tar ball with the entire contents of this directory
binsem.h Binary semaphore
critical.h Check mutual exclusion on critical sections
for.h Some handy macros
gensem.h General sempahore
monitor.h Monitor & Condition variables
fig2_5.prom Computer with registers
fig2_7.prom Inductive proofs of correctness
fig3_2.prom First attempt at solving the mutual exclusion problem
fig3_3.prom Second attempt at solving the mutual exclusion problem
fig3_4.prom Third attempt at solving the mutual exclusion problem
fig3_5.prom Fourth attempt at solving the mutual exclusion problem
fig3_6.prom Dekker's algorithm
fig3_7.prom Simplified Bakery algorithm
fig3_8.prom Bakery algorithm
fig3_10.prom Mutual exclusion with Test_and_Set
fig3_12.prom Mutual exclusion with Exchange
fig3_13.prom Peterson's algorithm for mutual exclusion
fig4_1.prom Mutual exclusion with semaphores
fig4_2.prom Mutual exclusion with process based semaphores
fig4_3.prom Producer-consumer with "infinite" buffer
fig4_5.prom Semaphores solution for "infinite" buffers
fig4_8.prom Semaphores solution for circular buffers
fig4_9.prom Circular buffer with binary semaphores
fig5_1.prom Monitor for producer-consumer
fig5_3.prom Emulation of semaphores by monitors
fig5_5.prom Monitor for Readers and writers
fig6_3.prom Dining Philosophers
fig6_4.prom Limit the number of philosophers
fig6_5.prom Asymmetric solution to dining philosophers
fig6_6.prom Monitor for dining philosophers
fig8_2.prom Degenerate bounder buffer
fig8_3.prom Bounded buffer
fig9_5.prom Matrix Multiplication Occam style
fig10_6.prom Matrix Multiplication Linda style
fig11_1.prom Distributed Mutual Exclusion
fig12_8.prom Distributed Termination -- Dijkstra Scholten
fig12_9.prom as fig12_8.prom but holding on to the semaphores longer
Name Last modified Size Description
Parent Directory 08-Apr-2005 15:03 -
ben-ari.tar 05-Feb-2005 16:10 90k tar archive
binsem.h 05-Feb-2005 16:10 1k