CHESS-Producer Consumer

Official Microsoft CHESS Page

Click here to go to the official CHESS page at Microsoft Research.

Original Code in C

The original code for the producer-consumer algorithm was written in C. The original author is unknown to me, but the code was given to me by Ganesh Gopolakrishnan when I joined his group.

prodcon.c

1   #include <pthread.h>
2   #include <stdio.h>
3   #include <assert.h>
4   
5   #define QUEUE_FULL_SIZE 1
6   
7     // global variables
8   pthread_mutex_t mux;
9   pthread_cond_t  cond_full;
10  pthread_cond_t  cond_empty;
11  
12  int qsize;
13  
14  int static counter = 0;
15  
16    // producer thread
17  void* producer(int * procid) {
18    int i;
19    for (i = 0; i < 1; i ++) {
20      pthread_mutex_lock(&mux);
21      while (qsize == QUEUE_FULL_SIZE)
22        pthread_cond_wait(&cond_full, &mux);
23      counter ++;
24      pthread_cond_signal(&cond_empty);
25      qsize ++;    
26      pthread_mutex_unlock(&mux);
27    }
28    return NULL;
29  }
30  
31  
32    // consumer thread
33  void* consumer(int * procid) {
34    int val, i;
35    for (i = 0; i < 1; i ++) {
36      pthread_mutex_lock(&mux);
37      while (qsize == 0)
38        pthread_cond_wait(&cond_empty, &mux);
39      pthread_cond_signal(&cond_full);
40      qsize --;
41      pthread_mutex_unlock(&mux);
42    }
43    return NULL;
44  }
45  
46  
47    // main procedure
48  int main() {
49    int i, ret1, ret2;
50    pthread_t prod[2];
51    pthread_t cons[2];
52    qsize = 0;
53  
54    pthread_mutex_init(&mux, NULL);
55    pthread_cond_init(&cond_full, NULL);
56    pthread_cond_init(&cond_empty, NULL);
57  
58    for (i = 0; i < 2; i ++) {
59      ret1 = pthread_create(&prod[i], NULL, 
60                                        producer, &i);
61      ret2 = pthread_create(&cons[i], NULL, 
62                                        consumer, &i);
63      if (ret1 != 0 || ret2 != 0)
64        exit(-1);
65    }
66    for (i = 0; i < 2; i ++) {
67      pthread_join(prod[i], NULL);
68      pthread_join(cons[i], NULL);
69    }
70  
71    pthread_mutex_destroy(&mux);
72    pthread_cond_destroy(&cond_full);
73    pthread_cond_destroy(&cond_empty);
74    return 0; 
75  }

You may download this C code here.

This code has been previously tested using Inspect created by Ganesh's Group. The results can be found here.

Ported into C#

C# is somewhat similar to C, but C is not an object-oriented programming language whereas C# is. There are many changes needed to transform this code into an object-oriented program.

In order to perform mutexes and conditional variables in C#, you need to use the Monitor class inside of the System.Threading namespace, which takes any object at all. For this program, I will just use strings as my mutexes and conditional variables. There also exists a Mutex class in C#, but the Monitor class will do for our needs.

Another change I will introduce is to create a class called Society that can produce and can consume.

The Society class

1   using System.Threading;
2   using Microsoft.VisualStudio.TestTools.UnitTesting;
3   
4   namespace TestProdCons {
5     public class Society {
6       public int full;
7       public int empty;
8       public int currentQuantity;
9         // Maximum amt each producer & consumer will 
10        //   run
11      public int maxRuns;
12        // Mutex and Conditional Variable for 
13        //   producers and consumers.
14      public object sharedMutex;
15        
16      public Society(int amt, int max) {
17        this.sharedMutex = "Shared Mutex";
18        this.currentQuantity = amt;
19        this.full = 2;
20        this.empty = 0;
21        this.maxRuns = max;
22      }
23  
24      public virtual void Produce() {
25        for (int i = 0; i < this.maxRuns; i++) {
26          try {
27              // Obtain a lock on the shared mutex.
28            Monitor.Enter(this.sharedMutex);
29            while (this.currentQuantity == this.full)
30              Monitor.Wait(this.sharedMutex);
31            Monitor.PulseAll(this.sharedMutex);
32            this.currentQuantity++;
33            int tmp = this.currentQuantity;
34            Assert.IsFalse(tmp > full || tmp < empty);
35          }
36          catch (ThreadInterruptedException e) { }
37          catch (SynchronizationLockException e) { }
38            // Release the shared mutex.
39          finally { Monitor.Exit(this.sharedMutex); }
40        }
41      }
42  
43      public virtual void Consume() {
44        for (int i = 0; i < this.maxRuns; i++) {
45          try {
46              // Obtain a lock on the shared mutex.
47            Monitor.Enter(this.sharedMutex);
48            while (this.currentQuantity == this.empty)
49              Monitor.Wait(this.sharedMutex);
50            Monitor.PulseAll(this.sharedMutex);
51            this.currentQuantity--;
52            int tmp = this.currentQuantity;
53            Assert.IsFalse(tmp > full || tmp < empty);
54          }
55          catch (ThreadInterruptedException e) {}
56          catch (SynchronizationLockException e) {}
57            // Release the shared mutex.
58          finally { Monitor.Exit(this.sharedMutex); }
59        }
60      }
61    }
62  }

This C# code along with the test can be downloaded here.

My Computer Specifications

In order to perform these tests on this code, I used a laptop with the following specifications.

Hardware Specifications

Laptop x86 64-Bit
Model: Acer Extensa 4420-5963
Processor: AMD Athlon 64 Dual-Core 2.0 GHz
Memory: 1790MB RAM

Software Specifications

OS: MS Windows XP Home 32-Bit (5.1, Build 2600)
MS Visual Studio 2008 Version 9.0.211022.8 RTM
MS .NET Framework Version 3.5
MS CHESS Version 0.1.30109.0 (32-Bit)(x86)

CHESS Test #1

In order to test the capabilities of CHESS, I introduced a mistake in the Society class. This mistake was placed in the Produce method of the Society class. The resulting class was saved as SocietyWithError1 that implements Society but overwrites the Produce method. It also overwrites the Consume method because Assert statements are inserted into both the Produce and Consume methods for testing purposes. The mistake is marked below.

The SocietyWithError1 class

1   using System.Threading;
2   using Microsoft.VisualStudio.TestTools.UnitTesting;
3   
4   namespace TestProdCons{
5     public class SocietyWithError1 : Society {
6       
7       public SocietyWithError1(int amt, int max) 
8              : base(amt, max) {}
9       
10      public override void Produce() {
11        for (int i = 0; i < this.maxRuns; i++) {
12          try {
13              // Obtain a lock on the shared mutex.
14            Monitor.Enter(this.sharedMutex);
15            if (this.currentQuantity == this.full)
16              Monitor.Wait(this.sharedMutex);
17            Monitor.PulseAll(this.sharedMutex);
18            this.currentQuantity++;
19              // This is the test that was added.
20            int tmp = this.currentQuantity;
21            Assert.IsFalse(tmp > full || tmp < empty);
22          } 
23          catch (ThreadInterruptedException e) { }
24          catch (SynchronizationLockException e) { }
25            // Release the shared mutex.
26          finally { Monitor.Exit(this.sharedMutex); }
27        }
28      }
29    }
30  }

Now that we have introduced an error, we need to create a test method for CHESS to digest. For this example, I want to have two producers and two consumers each running two times. The test method is part of the ProdConTest class.

The ProdConTest Class

1   using System.Threading;
2   using Microsoft.VisualStudio.TestTools.UnitTesting;
3   
4   namespace TestProdCons {
5     [TestClass]
6     public class ProdConTest {
7       [TestMethod]
8       [HostType("Chess")]
9       public void TestProdCon1() {
10        Society myCity = new Society(1, 2);
11        Thread prod1 = 
12                new Thread(
13                     new ThreadStart(myCity.Produce));
14        Thread prod2 = 
15                new Thread(
16                     new ThreadStart(myCity.Produce));
17        Thread con1 = 
18                new Thread(
19                     new ThreadStart(myCity.Consume));
20        Thread con2 = 
21                new Thread(
22                     new ThreadStart(myCity.Consume));
23        prod1.Name = "Producer 1";
24        prod2.Name = "Producer 2";
25        con1.Name = "Consumer 1";
26        con2.Name = "Consumer 2";
27        
28        prod1.Start();
29        prod2.Start();
30        con1.Start();
31        con2.Start();
32        
33        prod1.Join();
34        prod2.Join();
35        con1.Join();
36        con2.Join();
37        
38        // The Assert statement is in the producer
39        //   method. If CHESS finds the correct 
40        //   interleaving, then it will say
41        //   there was an unhandled exception
42        //   that the Assert.IsFalse failed.  
43        //   That is a good thing to get.
44      }
45    }
46  }

CHESS found the interleaving that causes the unhandled exception of the Assert statement failing inside of the Producer method.

One correct interleaving is as follows:

Producer 1 adds one to the currentQuantity making the currentQuantity equal to two.
Producer 1 then restarts and goes inside of the if statement and stops on the Monitor.Wait method call.
Producer 2 then starts and goes inside of the if statement too and stops on the Monitor.Wait method call.
Consumer 1 removes one from the currentQuantity making the currentQuantity equal to one.
Consumer 1 Preempts after it releases the lock on the shared mutex.
Producer 1 starts again and adds one to the currentQuantity making the currentQuantity equal to two.
Producer 1 finishes.
Producer 2 starts again and adds one to the current Quantity making the currentQuantity equal to three.
The Assert statement in Producer 2 fails because the currentQuantity is bigger than the full limit.

CHESS Analyzes a Producer-Consumer Society