--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * concurrency example with deadlock
+ * adapted from "Concurrency: State Models & Java Programs", Jeff Magee & Jeff Kramer
+ *
+ * Note there need to be at least 2x buffer_size instances of either producers or
+ * consumers in order to produce the deadlock, which basically depends on
+ * a notification choice between a consumer and a producer in a context where
+ * only threads of the notifier type are still runnable
+ *
+ * This is a good benchmark for state management/matching in a small heap context.
+ * Higher numbers of buffer size and producers/consumers result in a nice
+ * state explosion
+ */
+public class BoundedBuffer {
+
+ static int BUFFER_SIZE = 1;
+ static int N_PRODUCERS = 4;
+ static int N_CONSUMERS = 4;
+
+ static Object DATA = "fortytwo";
+
+ //--- the bounded buffer implementation
+ protected Object[] buf;
+ protected int in = 0;
+ protected int out= 0;
+ protected int count= 0;
+ protected int size;
+
+ public BoundedBuffer(int size) {
+ this.size = size;
+ buf = new Object[size];
+ }
+
+ public synchronized void put(Object o) throws InterruptedException {
+ while (count == size) {
+ wait();
+ }
+ buf[in] = o;
+ //System.out.println("PUT from " + Thread.currentThread().getName());
+ ++count;
+ in = (in + 1) % size;
+ notify(); // if this is not a notifyAll() we might notify the wrong waiter
+ }
+
+ public synchronized Object get() throws InterruptedException {
+ while (count == 0) {
+ wait();
+ }
+ Object o = buf[out];
+ buf[out] = null;
+ //System.out.println("GET from " + Thread.currentThread().getName());
+ --count;
+ out = (out + 1) % size;
+ notify(); // if this is not a notifyAll() we might notify the wrong waiter
+ return (o);
+ }
+
+ //--- the producer
+ static class Producer extends Thread {
+ static int nProducers = 1;
+ BoundedBuffer buf;
+
+ Producer(BoundedBuffer b) {
+ buf = b;
+ setName("P" + nProducers++);
+ }
+
+ @Override
+ public void run() {
+ try {
+ while(true) {
+ // to ease state matching, we don't put different objects in the buffer
+ buf.put(DATA);
+ }
+ } catch (InterruptedException e){}
+ }
+ }
+
+ //--- the consumer
+ static class Consumer extends Thread {
+ static int nConsumers = 1;
+ BoundedBuffer buf;
+
+ Consumer(BoundedBuffer b) {
+ buf = b;
+ setName( "C" + nConsumers++);
+ }
+
+ @Override
+ public void run() {
+ try {
+ while(true) {
+ Object tmp = buf.get();
+ }
+ } catch(InterruptedException e ){}
+ }
+ }
+
+ //--- the test driver
+ public static void main(String [] args) {
+ readArguments( args);
+ //System.out.printf("running BoundedBuffer with buffer-size %d, %d producers and %d consumers\n", BUFFER_SIZE, N_PRODUCERS, N_CONSUMERS);
+
+ BoundedBuffer buf = new BoundedBuffer(BUFFER_SIZE);
+
+ for (int i=0; i<N_PRODUCERS; i++) {
+ new Producer(buf).start();
+ }
+ for (int i=0; i<N_CONSUMERS; i++) {
+ new Consumer(buf).start();
+ }
+ }
+
+ static void readArguments (String[] args){
+ if (args.length > 0){
+ BUFFER_SIZE = Integer.parseInt(args[0]);
+ }
+ if (args.length > 1){
+ N_PRODUCERS = Integer.parseInt(args[1]);
+ }
+ if (args.length > 2){
+ N_CONSUMERS = Integer.parseInt(args[2]);
+ }
+ }
+}
--- /dev/null
+target = BoundedBuffer
+
+# this should produce a deadlock
+target.args = 2,4,1
\ No newline at end of file
--- /dev/null
+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--;
+ }
+
+}
+
--- /dev/null
+listener=.listener.CGMonitor
+
+target = ConcurrentCount
--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+public class DiningPhil {
+
+ static class Fork {
+ }
+
+ static class Philosopher extends Thread {
+
+ Fork left;
+ Fork right;
+
+ public Philosopher(Fork left, Fork right) {
+ this.left = left;
+ this.right = right;
+ //start();
+ }
+
+ @Override
+ public void run() {
+ // think!
+ synchronized (left) {
+ synchronized (right) {
+ // eat!
+ }
+ }
+ }
+ }
+
+ static int nPhilosophers = 6;
+
+ public static void main(String[] args) {
+ if (args.length > 0){
+ nPhilosophers = Integer.parseInt(args[0]);
+ }
+
+ //Verify.beginAtomic();
+ Fork[] forks = new Fork[nPhilosophers];
+ for (int i = 0; i < nPhilosophers; i++) {
+ forks[i] = new Fork();
+ }
+ for (int i = 0; i < nPhilosophers; i++) {
+ Philosopher p = new Philosopher(forks[i], forks[(i + 1) % nPhilosophers]);
+ p.start();
+ }
+ //Verify.endAtomic();
+ }
+}
\ No newline at end of file
--- /dev/null
+target = DiningPhil
+
+search.class = .search.heuristic.BFSHeuristic
--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * example to catch numeric value rnge violations with the NumericValueChecker listener
+ */
+public class NumericValueCheck {
+
+ public static void main (String[] args){
+ double someVariable;
+
+ someVariable = 42; // what else
+
+ someVariable = 12345; // ..That's the number only an idiot would have on his luggage
+ }
+}
--- /dev/null
+target = NumericValueCheck
+
+listener = .listener.NumericValueChecker
+
+# NumericValueChecker configuration
+range.vars = 1
+range.1.var = NumericValueCheck.main(java.lang.String[]):someVariable
+range.1.min = 0
+range.1.max = 42
+
+++ /dev/null
-class Racer implements Runnable {
- int d = 42
-
- public void run () {
- doSomething(1001)
- d = 0 // (1)
- }
-
- static void main (String[] args){
- Racer racer = new Racer()
- Thread t = new Thread(racer)
- t.start()
-
- doSomething(1000)
- int c = 420 / racer.d // (2)
- println c
- }
-
- def doSomething (int n) {
- try {
- Thread.sleep(n)
- } catch (InterruptedException ix) {}
- }
-}
println("Groovy model-checking")
Random random = new Random(42);
- int a = random.nextInt(2)
- int b = random.nextInt(3)
+ int a = random.nextInt(10)
+ int b = random.nextInt(10)
println("a=" + a)
println(" b=" + b)
- int c = a/(b+a -2)
+ int c = a/(b+a -5)
println(" c=" + c)
}
}
target = Rand
cg.enumerate_random = true
-report.console.property_violation=error,trace
+#report.console.property_violation=error,trace
--- /dev/null
+// This function runs when the SmartApp is installed
+def installed(a, b, c) {
+ println("a=" + a)
+ initialize(a, b, c)
+}
+
+// This function is where you initialize callbacks for event listeners
+def initialize(a, b, c) {
+ println(" b=" + b)
+ finalize(a, b, c)
+}
+
+def finalize(a, b, c) {
+ println(" c=" + c)
+ result(a, b, c)
+}
+
+def result(a, b, c) {
+ int d = a/(b+c-10)
+ println(" d=" + d)
+}
+
+Random random = new Random(42)
+int a = random.nextInt(10)
+int b = random.nextInt(10)
+int c = random.nextInt(10)
+installed(a,b,c)
+println "End of call!"
\ No newline at end of file
--- /dev/null
+target = RandComplex
+cg.enumerate_random = true
+#report.console.property_violation=error,trace
--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * example to show how to explore off-nominal paths
+ */
+public class StopWatch {
+
+ public static void main(String[] args){
+ long tStart = System.currentTimeMillis();
+ System.out.println("some lengthy computation..");
+ long tEnd = System.currentTimeMillis();
+
+ if (tEnd - tStart > 1000){
+ throw new RuntimeException("it took too long..");
+ }
+
+ System.out.println("all fine, finished in time");
+ }
+}
--- /dev/null
+target = StopWatch
+
+listener = .listener.StopWatchFuzzer
--- /dev/null
+target = TestExample
+
+listener=.listener.CoverageAnalyzer
+
+coverage.include = T1,T2
+coverage.show_methods = true
+#coverage.show_bodies = true
\ No newline at end of file
--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+class T1 {
+ int d = 42;
+
+ public int func1(int a, int b) {
+ if (a > b) {
+ return 1;
+ } else if (a == b) {
+ return 0;
+ } else {
+ return -1;
+ }
+ }
+
+ public boolean func2(boolean cond) {
+ if (cond && (d > 40)) {
+ d--;
+ } else {
+ d++;
+ }
+ return cond;
+ }
+}
+
+class T2 {
+
+ public int computeSomething (int a, int b){
+ try {
+ return a / b;
+ } catch (ArithmeticException ax){
+ return -1; // pretty lame error handling
+ }
+ }
+
+ public void doSomething() {
+ System.out.println("something");
+ }
+}
+
+public class TestExample {
+
+ public static void main(String[] args) {
+ T1 t1 = new T1();
+
+ assert t1.func1(1, 0) > 0;
+ assert t1.func1(0, 1) < 0;
+
+ assert t1.func2(true) == true;
+ assert t1.func2(false) == false;
+
+
+ T2 t2 = new T2();
+
+ assert t2.computeSomething(42, 42) == 1.0;
+ }
+}
+
--- /dev/null
+#!/bin/bash
+java -classpath ../build/jpf.jar gov.nasa.jpf.JPF +classpath=.:./groovy-2.5.7 $1
--- /dev/null
+#!/bin/bash
+java -classpath build/jpf.jar gov.nasa.jpf.JPF +classpath=examples:examples/groovy-2.5.7 $1
projects / jpf-core.git / commitdiff