module buffer(*implements circular buffers*const (*buffer size*var ninoutintegerbufarray of charprocedure deposit (xchar)begin if then halt endinc( )buf[in:xin :(in mod end depositprocedure fetch (var xchar)begin if then halt enddec( ) :buf[out]out :(out mod end fetchbegin : in : out : end buffer this simple implementation of buffer is acceptable onlyif the procedures deposit and fetch are activated by single agent (once acting as produceronce as consumerifhoweverthey are activated by individualconcurrent processesthis scheme is too simplistic the reason is that the attempt to deposit into full bufferor the attempt to fetch from an empty bufferare quite legitimate the execution of these actions will merely have to be delayed until the guarding conditions are established such delays essentially constitute the necessary synchronization among concurrent processes we may represent these delays respectively by the statements repeat until repeat until which must be substituted for the two conditioned halt statements buffering between concurrent processes the presented solution ishowevernot recommendedeven if it is known that the two processes are driven by two individual engines the reason is that the two processors necessarily access the same variable nand therefore the same store the idling processby constantly polling the value nand therefore the same store the idling processby constantly polling the value nhinders its partnerbecause at no time can the store be accessed by more than one process this kind of busy waiting must indeed be avoidedand we therefore postulate facility that makes the details of synchronization less explicitin fact hides them we shall call this facility signaland assume that it is available from utility module signals together with set of primitive operators on signals every signal is associated with guard (conditionps if process needs to be delayed until ps is established (by some other process)it mustbefore proceedingwait for the signal this is to be expressed by the statement wait(sifon the other handa process establishes psit thereupon signals this fact by the statement send(sif ps is the established precondition to every statement send( )then ps can be regarded as postcondition of wait(sdefinition signalstype signalprocedure wait (var ssignal)procedure send (var ssignal)procedure init (var ssignal)end signals