From: Manish Kumar Thakur <manish3499@gmail.com>
Date: Mon, 25 Mar 2019 13:37:07 +0000 (-0700)
Subject: Implements a jpf example ConcurrentCount (#177)
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=16956ee553b03f989c8e09d3df9b35ce21c10fa2;hp=e734381a6e606354034111dc855be9a8e454ce71

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
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
index 0000000..78cb235
--- /dev/null
+++ b/src/examples/ConcurrentCount.jpf
@@ -0,0 +1 @@
+target = ConcurrentCount