Your solution for this assignment should terminate within 10 seconds (when running ./pan). If they exceed the time limit, you will get partial credit. Please also note how long your solutions take to run as a comment if they do exceed the time limit.

The Producer-Consumer Problem

The producer-consumer problem is a classic scenario in distributed systems involving two processes:

1. The producer, which writes data into the shared buffer.
2. The consumer, which reads from the shared buffer.

A good solution to this problem should satisfy the following three properties:

1. Mutual exclusion: The producer and consumer processes never access the shared buffer simultaneously.
2. Non-starvation: The consumer accesses the buffer infinitely often. (You may assume that the producer never runs out of data to supply, and the consumer never stops attempting to read new data.)
3. Producer-consumer:
   • The producer never overwrites the data buffer unless the consumer has already read the current data
   • The consumer never reads the data buffer unless it contains new data.

The usual algorithm for producer-consumer uses a single flag bit. The flag bit is set by the producer when data ready to be read, and unset by the consumer once it has read the data. For the sake of this assignment, we only need to model whether the data buffer has been read, rather than modeling the contents of the data. We will use a single bit for this.

Your task is to model this algorithm in Promela, and then verify the above properties about it. It will help to remember that (1) and (3) are safety properties, but (2) is a liveness property. You may use both LTL and in-line assertions where appropriate.

Fill in the template below and add verifications for these properties. You should be able to run both ./pan and ./pan -a with no errors.

// Real bits in the algorithm:
// (1) The Boolean flag, indicating that there is data to be read.
bool flag = 0;

// For verification only
// (1) Who is in the "Critical Section", which is the parts of the program that can access
// the shared data
bool in_cs[2];
// (2) A Boolean that indicates whether the data in the buffer is unread.
//    NOTE: you are not required to model the buffer itself, only whether its data is fresh!
bool data = 0;

// Two processes ("active" means to load on startup). Recall that _pid is the unique process
// id assigned by Spin, starting at 0. 
active proctype Producer() {

}

active proctype Consumer() {

}

Below is a summary of commands and information you may need:

• <file>.pml : a Promela file
• spin <file>.pml : executes a single random simulation run
• spin -a <file>.pml : generates the verifier C program as pan.c
• gcc -o pan pan.c : compiles the verifier C program (with many options available!)
• ./pan : checks for deadlocks and violated assertions over all simulations
• ./pan -a : checks for the above plus violated LTL liveness properties
• spin -t -p <file>.pml : produces a counterexample trace produced by verifier

Handing In

Run cs195y_handin mc1 from a directory holding your Promela file (producer-consumer.pml). You should receive an email confirming that your handin has worked.