Your solutions 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 processes access 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 three assertions for these three 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() {

}

Chomp

In lab 3, you modeled the game Chomp in Alloy. This time around we'll model it in Promela which will greatly improve the runtime performance.

The rules of the game remain the same. In each turn, a player picks a row or column at which to break the candy bar, and the candy bar used for the following turn is whatever remains above the row that was broken off, or to the left of the column that was broken off. In alternating turns, players one and two choose rows or columns to break off such that their opponent is left with the soap (thereby losing the game). You can assume that we start with a non-square board.

Your task is to write two players that will play Chomp against each other. One player should be a player that always tries to create a square board on its turn. The other player is a free player that takes a random number of columns or rows on its turn.

In addition, you should write one assertion somewhere in your spec to verify that the winning strategy is indeed a winning stratagy assuming a non-square starting board.

Here's a template to get you started. You should be able to run ./pan with no errors.

//define the player turns
#define ATURN 1
#define BTURN 2

proctype SquarePlayer(byte turn) {
   //code for player that makes a square board each turn goes here.
}

proctype FreePlayer(byte turn) {
   //code for player that makes random choices each turn goes here
}

init {
   //Setup the board here. You should require a non-square starting board.

   //play the players against each other here.
}

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

Handing In

Run cs1950y_handin mc from a directory holding your Promela files (producer-consumer.pml and chomp.pml). You should receive an email confirming that your handin has worked.