Producer-Consumer System

Logic Model (Producer-Consumer System) Template:LogicModel 08 25, 2021
Abstract Specification Context The inherent non-determinism of concurrent systems results in bugs that occur extremely rarely and are not reproducible. Goal A buffer holds the data created by producing threads until they are retrieved by consuming threads. The buffer acts as a synchronizer, blocking and suspending threads when there is nothing for them to do. When the buffer is empty, any consuming thread needs to be blocked until there is data in the buffer. Conversely, if the buffer has a finite capacity, producing threads must be suspended when the buffer is full. Success Criteria At least one producer At least one consumer No thread is both consumer and producer Buffer capacity is at least 1 The type of data is nonempty
Concrete Implementation Given Inputs When Process is executed... Then, we get Outputs the (nonempty) set of producers the (nonempty) set of consumers the maximum number of messages in the bounded buffer the set of values that can be produced and/or consumed Producer-Consumer System/Design Producer-Consumer System/Write TLA Spec Producer-Consumer System/TLC Model Checking Producer-Consumer System/Intepret Error Trace Producer-Consumer System/Finish A shared buffer in a system of producers and consumers
Boundary/Safety Conditions of Producer-Consumer System Producer-Consumer System/Boundary