Implements a jpf example ConcurrentCount (#177)

* Implements the jpf example ConcurrentCount

* check for concurrency issue

diff --git a/src/examples/ConcurrentCount.java b/src/examples/ConcurrentCount.java
new file mode 100644 (file)
index 0000000..cedfd4e
--- /dev/null
+++ b/src/examples/ConcurrentCount.java
@@ -0,0 +1,59 @@
+import java.util.concurrent.atomic.AtomicBoolean;
+
+public class ConcurrentCount {
+       static final int COUNT = 30000;
+       volatile static int count = COUNT;
+       volatile static AtomicBoolean lock = new AtomicBoolean(false); 
+       static int a = 0;
+       static int b = 0;
+       
+       public static void main(String args[]) {
+               
+               new Thread() {
+                       
+                       @Override
+                       public void run() {
+                               while(count > 0) {
+                                       if (lock.get()) continue;
+                                       lock.set(true);
+                                       decreaseCount();
+                                       a++;
+                                       lock.set(false);
+                                       
+                                       
+                               }
+                       }
+               }.start();
+               
+        new Thread() {
+                       
+                       @Override
+                       public void run() {
+                               while(count > 0) {
+                                       if (lock.get()) continue;
+                                       lock.set(true);
+                                       decreaseCount();
+                                       b++;
+                                       lock.set(false);
+                                       
+                                       
+                               }
+                       }
+               }.start();
+               
+               while(count > 0);
+               //System.out.println("a = " + a);
+               //System.out.println("b = " + b);
+               //System.out.println("a + b = " + (a + b));
+               //System.out.println("count = " + count);
+
+               //Checks for concurrency error (which should be found when using model checking)
+               assert a + b == COUNT;
+       }
+       
+       private static synchronized void decreaseCount() {
+               count--;
+       }
+
+}
+

diff --git a/src/examples/ConcurrentCount.jpf b/src/examples/ConcurrentCount.jpf
new file mode 100644 (file)
index 0000000..78cb235
--- /dev/null
+++ b/src/examples/ConcurrentCount.jpf
@@ -0,0 +1 @@
+target = ConcurrentCount