Add basic concurrency support

Author: dcattaruzza

src/main/java/java/lang/IllegalThreadStateException.java

@@ -0,0 +1,50 @@
+/*
+ * Copyright (c) 1994, 2008, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+public class IllegalThreadStateException extends IllegalArgumentException {
+    private static final long serialVersionUID = -7626246362397460174L;
+
+    public IllegalThreadStateException() {
+        super();
+    }
+
+    public IllegalThreadStateException(String s) {
+        super(s);
+    }
+
+    // DIFFBLUE MODEL LIBRARY
+    // While Object.getClass() is not modelled, we can get the same
+    // functionality by adding one toString() method per subclass of
+    // Throwable.
+    @Override
+    public String toString() {
+        String message = getLocalizedMessage();
+        return (message != null)
+            ? ("java.lang.IllegalThreadStateException: " + message)
+            : "java.lang.IllegalThreadStateException";
+    }
+}

src/main/java/java/lang/Object.java

@@ -26,8 +26,20 @@
 package java.lang;
 
 import org.cprover.CProver;
+import java.lang.NullPointerException;
+import java.lang.IllegalMonitorStateException;
 
 public class Object {
+
+    // lock needed for synchronization in cbmc
+    // used by monitorenter, monitorexit, wait, and notify
+    // Not present in the original Object class
+    public int monitorCount;
+    
+    public Object() {
+      monitorCount = 0;
+    }
+    
     public final Class<?> getClass() {
       /*
        * MODELS LIBRARY {
@@ -57,11 +69,20 @@ public String toString() {
         return getClass().getName() + "@" + Integer.toHexString(hashCode());
     }
 
-    public final void notify() {}
+    public final void notify()
+    {
+      // FIXME: the thread must own the lock when it calls notify
+    }
 
-    public final void notifyAll() {}
+    // See implementation of notify
+    public final void notifyAll()
+    {
+      // FIXME: the thread must own the lock when it calls notifyAll
+    }
 
     public final void wait(long timeout) throws InterruptedException {
+      // FIXME: the thread must own the lock when it calls wait
+      // FIXME: should only throw if the interrupted flag in Thread is enabled
       throw new InterruptedException();
     }
 
@@ -87,4 +108,51 @@ public final void wait() throws InterruptedException {
     }
 
     protected void finalize() throws Throwable { }
+
+    /**
+     * This method is not present in the original Objecct class.
+     * It will be called by JBMC when the monitor in this instance
+     * is being acquired as a result of either the execution of a
+     * monitorenter bytecode instruction or the call to a synchronized
+     * method. It uses a counter to enable reentrance and an atomic section
+     * to ensure multiple threads do not race in the access/modification of
+     * the counter.
+     */
+    public static void monitorenter(Object object)
+    {
+      //FIXME: we shoud remove the call to this method from the call
+      // stack appended to the thrown exception
+      if (object == null)
+        throw new NullPointerException();
+
+      CProver.atomicBegin();
+      // this assume blocks this execution path in JBMC and simulates
+      // the thread having to wait because the monitor is not available
+      CProver.assume(object.monitorCount == 0);
+      object.monitorCount++;
+      CProver.atomicEnd();
+    }
+
+    /**
+     * This method is not present in the original Objecct class.
+     * It will be called by JBMC when the monitor in this instance
+     * is being released as a result of either the execution of a
+     * monitorexit bytecode instruction or the return (normal or exceptional)
+     * of a synchronized method. It decrements the monitorCounter that had
+     * been incremented in monitorenter().
+     */
+    public static void monitorexit(Object object)
+    {
+      //FIXME: we shoud remove the call to this method from the call
+      // stack appended to the thrown exception
+      if (object == null)
+        throw new NullPointerException();
+
+      if (object.monitorCount == 0)
+        throw new IllegalMonitorStateException();
+      CProver.atomicBegin();
+      object.monitorCount--;
+      CProver.atomicEnd();
+    }
+
 }

src/main/java/java/lang/Runnable.java

@@ -0,0 +1,69 @@
+/*
+ * Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.lang;
+
+/**
+ * The <code>Runnable</code> interface should be implemented by any
+ * class whose instances are intended to be executed by a thread. The
+ * class must define a method of no arguments called <code>run</code>.
+ * <p>
+ * This interface is designed to provide a common protocol for objects that
+ * wish to execute code while they are active. For example,
+ * <code>Runnable</code> is implemented by class <code>Thread</code>.
+ * Being active simply means that a thread has been started and has not
+ * yet been stopped.
+ * <p>
+ * In addition, <code>Runnable</code> provides the means for a class to be
+ * active while not subclassing <code>Thread</code>. A class that implements
+ * <code>Runnable</code> can run without subclassing <code>Thread</code>
+ * by instantiating a <code>Thread</code> instance and passing itself in
+ * as the target.  In most cases, the <code>Runnable</code> interface should
+ * be used if you are only planning to override the <code>run()</code>
+ * method and no other <code>Thread</code> methods.
+ * This is important because classes should not be subclassed
+ * unless the programmer intends on modifying or enhancing the fundamental
+ * behavior of the class.
+ *
+ * @author  Arthur van Hoff
+ * @see     java.lang.Thread
+ * @see     java.util.concurrent.Callable
+ * @since   JDK1.0
+ */
+@FunctionalInterface
+public interface Runnable {
+    /**
+     * When an object implementing interface <code>Runnable</code> is used
+     * to create a thread, starting the thread causes the object's
+     * <code>run</code> method to be called in that separately executing
+     * thread.
+     * <p>
+     * The general contract of the method <code>run</code> is that it may
+     * take any action whatsoever.
+     *
+     * @see     java.lang.Thread#run()
+     */
+    public abstract void run();
+}