From d93606fa078221b7de93c02bb963b5b7875c2a8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Apr 2016 22:25:43 +0200
Subject: [PATCH] using Random to model threads
---
library/util/Random.scala | 1 -
testcases/verification/xlang/DataRacing.scala | 42 +++++++++++++++++++
2 files changed, 42 insertions(+), 1 deletion(-)
create mode 100644 testcases/verification/xlang/DataRacing.scala
diff --git a/library/util/Random.scala b/library/util/Random.scala
index e055dc51b..8a942e31b 100644
--- a/library/util/Random.scala
+++ b/library/util/Random.scala
@@ -29,4 +29,3 @@ object Random {
} ensuring(res => res >= 0 && res < max)
}
-
diff --git a/testcases/verification/xlang/DataRacing.scala b/testcases/verification/xlang/DataRacing.scala
new file mode 100644
index 000000000..259295594
--- /dev/null
+++ b/testcases/verification/xlang/DataRacing.scala
@@ -0,0 +1,42 @@
+import leon.lang._
+import leon.lang.xlang._
+import leon.util.Random
+
+import leon.collection._
+
+object DataRacing {
+
+ case class SharedState(var i: Int)
+
+ case class AtomicInstr(instr: (SharedState) => Unit)
+
+ implicit def toInstr(instr: (SharedState) => Unit): AtomicInstr = AtomicInstr(instr)
+
+
+ def execute(t1: List[AtomicInstr], t2: List[AtomicInstr], state: SharedState): Unit = (t1, t2) match {
+ case (x::xs, y::ys) =>
+ if(Random.nextBoolean) {
+ x.instr(state)
+ execute(xs, y::ys, state)
+ } else {
+ y.instr(state)
+ execute(x::xs, ys, state)
+ }
+ case (Nil(), y::ys) =>
+ y.instr(state)
+ execute(Nil(), ys, state)
+ case (x::xs, Nil()) =>
+ x.instr(state)
+ execute(xs, Nil(), state)
+ case (Nil(), Nil()) => ()
+ }
+
+ def main(): Unit = {
+ val state = SharedState(0)
+ val t1 = List[AtomicInstr]((s: SharedState) => s.i = s.i + 1)
+ val t2 = List[AtomicInstr]((s: SharedState) => s.i = s.i * 2)
+ execute(t1, t2, state)
+ assert(state.i == 2)
+ }
+
+}
--
GitLab