CHESS Analyzes an Unbounded Lock Free Queue
Official Microsoft CHESS Page
Click here to go to the official CHESS page at Microsoft Research.
Original Code in Java
This Java code can be downloaded here.
The original code for the Unbounded Lock-Free Queue came from The Art of Multiprocessor Programming by Maurice Herlihy & Nir Shavit, chapter 10. Their code was originally expressed using Java code.
The EmptyException Class
1 package unbounded_lockfree_queue;
2 public class EmptyException extends Exception {}
The Node Class
1 package unbounded_lockfree_queue;
2
3 import java.util.concurrent.atomic.AtomicReference;
4
5 public class Node<T> {
6 public T value;
7 public AtomicReference<Node<T>> next;
8 public Node (T value) {
9 this.value = value;
10 this.next = new AtomicReference<Node<T>>(null);
11 }
12 }
The LockFreeQueue Class
1 package unbounded_lockfree_queue;
2
3 import java.util.concurrent.atomic.AtomicReference;
4
5 public class LockFreeQueue<T> {
6 AtomicReference<Node<T>> head, tail;
7
8 public LockFreeQueue () {
9 Node<T> node = new Node<T>(null);
10 head.set(node);
11 tail.set(node);
12 }
13
14 public void enq (T value) {
15 Node<T> node = new Node<T>(value);
16 while(true) {
17 Node<T> last = tail.get();
18 Node<T> next = last.next.get();
19 if (last == tail.get()) {
20 if (next == null) {
21 if (last.next.compareAndSet(next, node)) {
22 tail.compareAndSet(last, node);
23 return;
24 }
25 } else {
26 tail.compareAndSet(last, next);
27 }
28 }
29 }
30 }
31
32 public T deq() throws EmptyException {
33 while (true) {
34 Node<T> first = head.get();
35 Node<T> last = tail.get();
36 Node<T> next = first.next.get();
37 if (first == head.get()) {
38 if (first == last) {
39 if (next == null)
40 throw new EmptyException();
41 tail.compareAndSet(last, next);
42 } else {
43 T value = next.value;
44 if (head.compareAndSet(first, next))
45 return value;
46 }
47 }
48 }
49 }
50 }
A few peices of code were added to the original code provieded in The Art of Multiprocessor Programming so that the code could compile. These were only minor changes and do not affect the main content or ideas of the author's code.
This Java code can be downloaded here.
Ported into C#
C# is similar to Java in programming style. There are a few differences to note when transfering this code from Java to C#.
This C# code along with all of the tests can be downloaded here.
In C#, there is no equivalent class for Java's AtomicReference. In order to have the functionality of compareAndSet on object references in C#, you must use the Interlocked class inside of the System.Threading namespace. The method for compareAndSet is CompareExchange in the Interlocked class, and it's a static method. Because of this, we will be using simple object references instead of atomic references. This is the main difference.
The EmptyException class
1 using System;
2
3 namespace TestLockFreeQueue {
4 public class EmptyException : Exception {}
5 }
The Node class
1 namespace TestLockFreeQueue {
2 public class Node<T> where T : class {
3 public T val;
4 public Node<T> next;
5 public Node (T val) {
6 this.val = val;
7 this.next = null;
8 }
9 }
10 }
The LockFreeQueue class
1 using System.Threading;
2
3 namespace TestLockFreeQueue {
4 public class LockFreeQueue<T> where T : class {
5 public Node<T> head, tail;
6 public LockFreeQueue () {
7 Node<T> node = new Node<T>(null);
8 head = tail = node;
9 }
10
11 public virtual void enq(T x) {
12 Node<T> node = new Node<T>(x);
13 while (true) {
14 Node<T> last = tail;
15 Node<T> next = last.next;
16 if (last == tail) {
17 if (next == null) {
18 if (next == Interlocked.CompareExchange(
19 ref last.next,node,next)) {
20 Interlocked.CompareExchange(ref tail,
21 node, last);
22 return;
23 }
24 } else {
25 Interlocked.CompareExchange(ref tail,
26 next, last);
27 }
28 }
29 }
30 }
31
32 public virtual T deq() {
33 while (true) {
34 Node<T> first = head;
35 Node<T> last = tail;
36 Node<T> next = first.next;
37 if (first == head) {
38 if (first == last) {
39 if (next == null)
40 throw new EmptyException();
41 Interlocked.CompareExchange(ref tail,
42 next,last);
43 } else {
44 T val = next.val;
45 if (first ==
46 Interlocked.CompareExchange(
47 ref head,next,first))
48 return val;
49 }
50 }
51 }
52 }
53 }
54 }
This C# code along with all of the tests 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
This C# code along with all of the tests can be downloaded here.
In order to test the capabilities of CHESS, I introduced a mistake in the LockFreeQueue code. This mistake was placed in the enq() method of the LockFreeQueue class. The resulting class was saved as LockFreeQueueWithError1 that implements LockFreeQueue but overwrites the enq() method. The mistake is marked below.
The LockFreeQueueWithError1 class
1 using System.Threading;
2
3 namespace TestLockFreeQueue {
4 public class LockFreeQueueWithError1<T> :
5 LockFreeQueue<T> where T : class {
6 public override void enq(T x) {
7 Node<T> node = new Node<T>(x);
8 while (true) {
9 Node<T> last = tail;
10 Node<T> next = last.next;
11 if (last == tail) {
12 if (next == null) {
13 if (next == Interlocked.CompareExchange(
14 ref last.next,node,next)) {
15 // The mistake was introduced by
16 // replacing an atomic opperation
17 // (i.e. CompareExchange) with a
18 // non-atomic opperation.
19 if (tail == last)
20 tail = node;
21 return;
22 }
23 } else {
24 Interlocked.CompareExchange(ref tail,
25 next, last);
26 }
27 }
28 }
29 }
30 }
31 }
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 threads that each enqueue two Strings into a LockFreeQueue of Strings. The test method, along with helper methods and a Struct are all part of the QueueTest class.
At first, I used the default settings for CHESS, but it passed the test. I later found out that in order to preempt around important variables, you must mark the important variables as volatiles and tell CHESS to monitor volatiles.
Change to the LockFreeQueue Class
1 using System.Threading;
2
3 namespace TestLockFreeQueue {
4 public class LockFreeQueue<T> where T : class {
5 public volatile Node<T> head, tail;
6 ...
The QueueTest Class
1 using System;
2 using System.Threading;
3 using Microsoft.VisualStudio.TestTools.UnitTesting;
4
5 namespace TestLockFreeQueue {
6 [TestClass]
7 public class QueueTest {
8 public struct EnqContainer {
9 public String first;
10 public String second;
11 public LockFreeQueue<String> q;
12 }
13
14 public void EnqTwoStrings (Object o) {
15 EnqContainer e = (EnqContainer)o;
16 e.q.enq(e.first);
17 e.q.enq(e.second);
18 }
19
20 [TestMethod]
21 [HostType("Chess")]
22 [TestProperty("ChessMonitorVolatiles","True")]
23 public void TestLockFreeQueueWithError1(){
24 QueueTest qt = new QueueTest();
25 LockFreeQueue<String> lfq =
26 new LockFreeQueueWithError1<String>();
27 EnqContainer firstParams, secondParams;
28 firstParams.q = secondParams.q = lfq;
29 firstParams.first = "a";
30 firstParams.second = "b";
31 secondParams.first = "c";
32 secondParams.second = "d";
33 Thread t2 =
34 new Thread(new ParameterizedThreadStart(
35 qt.EnqTwoStrings));
36 t2.Start(secondParams);
37 EnqTwoStrings(firstParams);
38 t2.Join();
39 // Test - Verify that the head is
40 // connected to the tail and that
41 // the tail is exactly 4 nodes
42 // away from the head.
43 Node<String> current = lfq.head;
44 for (int i = 0; i < 4; i++)
45 current = current.next;
46 Assert.IsTrue (current == lfq.tail);
47 }
48 }
49 }
When I ran this test without telling CHESS to preempt around volatile variables, the test did not fail. I thought that it should fail, so I worked it out by hand. I have included a pdf version of an interleaving that makes the test fail.
lockfreequeue_byhand.pdf
After, I ran the code with CHESS and marked it to check the volatile variables. It found the same interleaving that I found by hand. In conclusion, CHESS was able to find the introduced mistake only if it is marked to moniter volatiles. It can be a useful tool for finding these race conditions.
This C# code along with all of the tests can be downloaded here.
Tutorail to repeat CHESS Test #1
Use Chess inside of Visual Studio.
This tutorial describes how to repeat the tests on LockFreeQueueWithError1 using Visual Studio 2008 and Microsoft Chess. Click here to view the tutorial.
Use the command-line tool MChess
This tutorial describes how to repeat the tests on LockFreeQueueWithError1 using the command-line tool MChess. Click here to view the tutorial.
CHESS Test #2
This C# code along with all of the tests can be downloaded here.
The second test is similar to the first one. I introduced a similar mistake; I swaped a CompareExchange method into a non-atomic if statement.
The LockFreeQueueWithError2 Class
1 using System.Threading;
2
3 namespace TestLockFreeQueue {
4 public class LockFreeQueueWithError2<T> :
5 LockFreeQueue<T> where T : class {
6 public override void enq(T x) {
7 Node<T> node = new Node<T>(x);
8 while (true) {
9 Node<T> last = tail;
10 Node<T> next = last.next;
11 if (last == tail) {
12 if (next == null) {
13 if (next == Interlocked.CompareExchange(
14 ref last.next,node,next)) {
15 Interlocked.CompareExchange (ref tail,
16 node, last);
17 return;
18 }
19 } else {
20 // The mistake was introduced by
21 // replacing an atomic opperation
22 // (i.e. CompareExchange) with a
23 // non-atomic opperation.
24 if (tail == last)
25 tail = next;
26 }
27 }
28 }
29 }
30 }
31 }
The error that could happen due to this mistake is quite different than the first one. For the mistake to show itself, we need to introduce a third thread that dequeues three items from the queue.
The QueueTest Class
1 using System;
2 using System.Threading;
3 using Microsoft.VisualStudio.TestTools.UnitTesting;
4
5 namespace TestLockFreeQueue {
6 [TestClass]
7 public class QueueTest {
8 public struct EnqContainer {
9 public String first;
10 public String second;
11 public LockFreeQueue<String> q;
12 }
13
14 public void EnqTwoStrings (Object o) {
15 EnqContainer e = (EnqContainer)o;
16 e.q.enq(e.first);
17 e.q.enq(e.second);
18 }
19
20 public void DeqThreeStrings(Object o) {
21 LockFreeQueue<String> lfq =
22 (LockFreeQueue<String>)o;
23 try { lfq.deq(); } catch (EmptyException e) {}
24 try { lfq.deq(); } catch (EmptyException e) {}
25 try { lfq.deq(); } catch (EmptyException e) {}
26 }
27
28 [TestMethod]
29 [HostType("Chess")]
30 [TestProperty("ChessMonitorVolatiles", "True")]
31 [TestProperty("ChessBound", "4")]
32 public void TestLockFreeQueueWithError2() {
33 QueueTest qt = new QueueTest();
34 LockFreeQueue<String> lfq =
35 new LockFreeQueueWithError2<String>();
36 EnqContainer firstParams, secondParams;
37 firstParams.q = secondParams.q = lfq;
38 firstParams.first = "a";
39 firstParams.second = "b";
40 secondParams.first = "c";
41 secondParams.second = "d";
42 Thread t2 = new Thread(
43 new ParameterizedThreadStart(
44 qt.EnqTwoStrings));
45 Thread t3 = new Thread(
46 new ParameterizedThreadStart(
47 qt.DeqThreeStrings));
48 t2.Start(secondParams);
49 t3.Start(lfq);
50 EnqTwoStrings(firstParams);
51 t2.Join();
52 t3.Join();
53 }
54 }
55 }
56
I removed the test at the end that tests if the head is connected to that tail, because no matter how you perform the interleavings, that will ALWAYS come out to be true.
What turns out happening is that the tail ends up behind the head and then the program runs another deq method in which, if you follow closely to what the method will do if the tail is behind the head and the next Node in front of the head is null, you will end up with a NullPointerException.
Unfortunately, in order to get a NullPointerException to occur with these three threads, four preemptions are required. The default preemption bound for CHESS is two. That is why I set the CHESS property ChessBound to 4 so that CHESS would check interleavings with up to four preemptions.
With the preemption bound set to four, three different threads to interleave, and CHESS is set to moniter the volatile variables, on my computer, this test took nearly 15 minutes until it ran into a NullPointerException, just like I had found by hand.
Before I developed the final version, I ran the test by hand. I have included a pdf version of the interleaving that I found causing a NullPointerException. I had to do this step in order to find out what kind of testing was neccissary to cause an error in the program due to the mistake introduced into the original code.
lockfreequeue2_byhand.pdf
This C# code along with all of the tests can be downloaded here.