Communicating Sequential Processes

acquire action alphabet alternative array backing store behaviour BLEEP buffer channel Chapter checkpoint choc chocolate coin Communicating Sequential Processes communication concealed concurrent processes constructed COPY critical region deadlock defined definition denote described deterministic processes divergence doub E. W. Dijkstra Edsger W engage ensure environment event Examples X1 following laws fork function guarded high-level programming language implementation in1p infinite initial value input interact interleaving introduced labelled laws L1 left2 line printer LISP livelock loop mathematical messages monitor mutual recursion natural numbers node nondeterminism nondeterministic process notation observation occur operand operating system output pair philosopher possible prefix process which behaves processor proof refuse release resource result S(tr satisfies scratch file Section selected sequence sequential processes sharing processes simultaneously single solution specification STOP storage subordinate process subroutine symbol terminate successfully tion toffee trace variable vending machine