diff --git a/libtest/pom.xml b/libtest/pom.xml index 344eb1f97..8f001f116 100755 --- a/libtest/pom.xml +++ b/libtest/pom.xml @@ -19,7 +19,6 @@ jctools-core 1.0 - org.openjdk.jmh jmh-core @@ -31,19 +30,16 @@ 0.6 provided - com.google.guava guava 18.0 - com.boundary high-scale-lib 1.0.6 - com.github.romix java-concurrent-hash-trie-map @@ -53,6 +49,13 @@ org.jetbrains.kotlinx lincheck ${project.version} + + + org.jetbrains.kotlinx + lincheck + ${project.version} + tests + test-jar test diff --git a/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Accounts.java b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Accounts.java new file mode 100644 index 000000000..815e9f6a2 --- /dev/null +++ b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Accounts.java @@ -0,0 +1,171 @@ +/* + * #%L + * libtest + * %% + * Copyright (C) 2015 - 2018 Devexperts, LLC + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom; + +import org.jetbrains.annotations.NotNull; +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; + +import java.util.HashMap; +import java.util.Map; + +public abstract class Accounts extends VerifierState { + protected Map data; + + public abstract Integer getAmount(int id); + public abstract void setAmount(int id, int value); + public abstract void transfer(int id1, int id2, int value); + + @NotNull + @Override + public Object extractState() { + return data; + } +} + +class AccountsWrong1 extends Accounts { + public AccountsWrong1() { + data = new HashMap<>(); + } + + @Override + public Integer getAmount(int id) { + if (data.containsKey(id)) { + return data.get(id); + } else { + return 0; + } + } + + @Override + public void setAmount(int id, int value) { + data.put(id, value); + } + + @Override + public synchronized void transfer(int id1, int id2, int value) { + if (id1 == id2) return; + Integer v1 = data.get(id1); + Integer v2 = data.get(id2); + if (v1 == null) v1 = 0; + if (v2 == null) v2 = 0; + v1 -= value; + v2 += value; + data.put(id1, v1); + data.put(id2, v2); + } +} + +class AccountsWrong2 extends Accounts { + public AccountsWrong2() { + data = new HashMap<>(); + } + + @Override + public Integer getAmount(int id) { + if (data.containsKey(id)) { + return data.get(id); + } else { + return 0; + } + } + + @Override + public synchronized void setAmount(int id, int value) { + data.put(id, value); + } + + @Override + public void transfer(int id1, int id2, int value) { + if (id1 == id2) return; + Integer v1 = data.get(id1); + Integer v2 = data.get(id2); + if (v1 == null) v1 = 0; + if (v2 == null) v2 = 0; + v1 -= value; + v2 += value; + data.put(id1, v1); + data.put(id2, v2); + } +} + +class AccountsWrong3 extends Accounts { + public AccountsWrong3() { + data = new HashMap<>(); + } + + @Override + public Integer getAmount(int id) { + if (data.containsKey(id)) { + return data.get(id); + } else { + return 0; + } + } + + @Override + public void setAmount(int id, int value) { + data.put(id, value); + } + + @Override + public void transfer(int id1, int id2, int value) { + if (id1 == id2) return; + Integer v1 = data.get(id1); + Integer v2 = data.get(id2); + if (v1 == null) v1 = 0; + if (v2 == null) v2 = 0; + v1 -= value; + v2 += value; + data.put(id1, v1); + data.put(id2, v2); + } +} + +class AccountsWrong4 extends Accounts { + public AccountsWrong4() { + data = new HashMap<>(1); + } + + // This operation is not synchronized with others + @Override + public Integer getAmount(int id) { + return data.getOrDefault(id, 0); + } + + @Override + public synchronized void setAmount(int id, int value) { + data.put(id, value); + } + + @Override + public synchronized void transfer(int id1, int id2, int value) { + if (id1 == id2) return; + Integer v1 = data.get(id1); + Integer v2 = data.get(id2); + if (v1 == null) v1 = 0; + if (v2 == null) v2 = 0; + v1 -= value; + v2 += value; + data.put(id1, v1); + data.put(id2, v2); + } +} diff --git a/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Counters.kt b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Counters.kt new file mode 100644 index 000000000..bafe197dc --- /dev/null +++ b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Counters.kt @@ -0,0 +1,66 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import java.util.concurrent.atomic.AtomicInteger + +interface Counter { + fun incrementAndGet(): Int + + fun get(): Int +} + +internal class CounterWrong0 : Counter { + private var c: Int = 0 + + override fun incrementAndGet(): Int = ++c + + override fun get(): Int = c +} + +internal class CounterWrong1 : Counter { + private var c: Int = 0 + + override fun incrementAndGet(): Int { + c++ + return c + } + + override fun get(): Int = c +} + +internal class CounterWrong2 : Counter { + @Volatile + private var c: Int = 0 + + override fun incrementAndGet(): Int = ++c + + override fun get(): Int = c +} + +internal class CounterCorrect : Counter { + private val c = AtomicInteger() + + override fun incrementAndGet(): Int = c.incrementAndGet() + + override fun get(): Int = c.get() +} \ No newline at end of file diff --git a/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSets.kt b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSets.kt new file mode 100644 index 000000000..a8e9b8bac --- /dev/null +++ b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSets.kt @@ -0,0 +1,104 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import java.util.concurrent.atomic.AtomicBoolean +import java.util.concurrent.locks.ReentrantLock +import kotlin.concurrent.withLock + +interface Set { + fun add(key: Int): Boolean + fun remove(key: Int): Boolean + fun contains(key: Int): Boolean +} + +internal class SpinLockBasedSet : Set { + private val set = mutableSetOf() + private val locked = AtomicBoolean() + + override fun add(key: Int): Boolean = withSpinLock { + set.add(key) + } + + override fun remove(key: Int): Boolean = withSpinLock { + set.remove(key) + } + + override fun contains(key: Int): Boolean = withSpinLock { + set.contains(key) + } + + private fun withSpinLock(block: () -> Boolean): Boolean { + while (!locked.compareAndSet(false, true)) { Thread.yield() } + try { + return block() + } finally { + locked.set(false) + } + } +} + +internal class ReentrantLockBasedSet : Set { + private val set = mutableSetOf() + private val lock = ReentrantLock() + + override fun add(key: Int): Boolean = lock.withLock { + set.add(key) + } + + override fun remove(key: Int): Boolean = lock.withLock { + set.remove(key) + } + + override fun contains(key: Int): Boolean = lock.withLock { + set.contains(key) + } +} + +internal class SynchronizedBlockBasedSet : Set { + private val set = mutableSetOf() + + override fun add(key: Int): Boolean = synchronized(set) { + set.add(key) + } + + override fun remove(key: Int): Boolean = synchronized(set) { + set.remove(key) + } + + override fun contains(key: Int): Boolean = synchronized(set) { + set.contains(key) + } +} + +internal class SynchronizedMethodBasedSet : Set { + private val set = mutableSetOf() + + @Synchronized + override fun add(key: Int): Boolean = set.add(key) + + @Synchronized + override fun remove(key: Int): Boolean = set.remove(key) + + @Synchronized + override fun contains(key: Int): Boolean = set.contains(key) +} \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDeque.java b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDeque.java similarity index 99% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDeque.java rename to libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDeque.java index 38eac5f3a..852acae1c 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDeque.java +++ b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDeque.java @@ -1,4 +1,4 @@ -package org.jetbrains.kotlinx.lincheck.tests; +package org.jetbrains.kotlinx.lincheck.tests.custom; /* * #%L @@ -26,7 +26,6 @@ // Double-linked list by Sundell public class LockFreeDeque { - private final Node head; private final Node tail; diff --git a/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Queue.java b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Queue.java new file mode 100644 index 000000000..bc38f6d0f --- /dev/null +++ b/libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Queue.java @@ -0,0 +1,216 @@ +/* + * #%L + * libtest + * %% + * Copyright (C) 2015 - 2018 Devexperts, LLC + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom; + +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; + +import java.util.ArrayList; +import java.util.List; + +public abstract class Queue extends VerifierState { + public abstract void put(int x) throws FullQueueException; + public abstract int get() throws EmptyQueueException; + + @Override + public Object extractState() { + List elements = new ArrayList<>(); + try { + while (true) { + elements.add(get()); + } + } catch (EmptyQueueException e) { + // queue is empry + } + return elements; + } + + public static class EmptyQueueException extends Exception {} + public static class FullQueueException extends Exception {} +} + +class QueueWrong1 extends Queue { + private int indGet; + private int indPut; + private int countElements; + + private int[] items; + + private int inc(int i) { + return (++i == items.length ? 0 : i); + } + + public QueueWrong1(int capacity) { + items = new int[capacity]; + + indPut = 0; + indGet = 0; + countElements = 0; + + } + + @Override + public void put(int x) throws FullQueueException { + if (countElements == items.length) { + throw new FullQueueException(); + } + items[indPut] = x; + indPut = inc(indPut); + countElements++; + } + + @Override + public int get() throws EmptyQueueException { + if (countElements == 0) { + throw new EmptyQueueException(); + } + int ret = items[indGet]; + indGet = inc(indGet); + countElements--; + return ret; + } +} + +class QueueWrong2 extends Queue { + private int indGet; + private int indPut; + private int countElements; + + private int[] items; + + private int inc(int i) { + return (++i == items.length ? 0 : i); + } + + public QueueWrong2(int capacity) { + items = new int[capacity]; + + indPut = 0; + indGet = 0; + countElements = 0; + + } + + @Override + public synchronized void put(int x) throws FullQueueException { + if (countElements == items.length) { + throw new FullQueueException(); + } + items[indPut] = x; + indPut = inc(indPut); + countElements++; + } + + @Override + public int get() throws EmptyQueueException { + if (countElements == 0) { + throw new EmptyQueueException(); + } + int ret = items[indGet]; + indGet = inc(indGet); + countElements--; + return ret; + } +} + +class QueueWrong3 extends Queue { + private int indGet; + private int indPut; + private int countElements; + + private int[] items; + + private int inc(int i) { + return (++i == items.length ? 0 : i); + } + + public QueueWrong3(int capacity) { + items = new int[capacity]; + + indPut = 0; + indGet = 0; + countElements = 0; + + } + + @Override + public void put(int x) throws FullQueueException { + if (countElements == items.length) { + throw new FullQueueException(); + } + items[indPut] = x; + indPut = inc(indPut); + countElements++; + } + + @Override + public synchronized int get() throws EmptyQueueException { + if (countElements == 0) { + throw new EmptyQueueException(); + } + int ret = items[indGet]; + indGet = inc(indGet); + countElements--; + return ret; + } +} + +class QueueSynchronized extends Queue { + private int indGet; + private int indPut; + private int countElements; + + private int[] items; + + private int inc(int i) { + return (++i == items.length ? 0 : i); + } + + public QueueSynchronized(int capacity) { + items = new int[capacity]; + + indPut = 0; + indGet = 0; + countElements = 0; + + } + + @Override + public synchronized void put(int x) throws FullQueueException { + if (countElements == items.length) { + throw new FullQueueException(); + } + items[indPut] = x; + indPut = inc(indPut); + countElements++; + } + + @Override + public synchronized int get() throws EmptyQueueException { + if (countElements == 0) { + throw new EmptyQueueException(); + } + int ret = items[indGet]; + indGet = inc(indGet); + countElements--; + return ret; + } +} diff --git a/libtest/src/main/java/tests/custom/counter/Counter.java b/libtest/src/main/java/tests/custom/counter/Counter.java deleted file mode 100644 index 10d33d600..000000000 --- a/libtest/src/main/java/tests/custom/counter/Counter.java +++ /dev/null @@ -1,27 +0,0 @@ -package tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public interface Counter { - public int incrementAndGet(); -} \ No newline at end of file diff --git a/libtest/src/main/java/tests/custom/counter/CounterGet.java b/libtest/src/main/java/tests/custom/counter/CounterGet.java deleted file mode 100644 index c1a57df9a..000000000 --- a/libtest/src/main/java/tests/custom/counter/CounterGet.java +++ /dev/null @@ -1,39 +0,0 @@ -package tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterGet{ - private int c; - - public CounterGet() { - c = 0; - } - - public int get() { - return c; - } - - public synchronized int incrementAndGet() { - return ++c; - } -} diff --git a/libtest/src/main/java/tests/custom/counter/CounterWrong0.java b/libtest/src/main/java/tests/custom/counter/CounterWrong0.java deleted file mode 100644 index b734ff5d8..000000000 --- a/libtest/src/main/java/tests/custom/counter/CounterWrong0.java +++ /dev/null @@ -1,38 +0,0 @@ -package tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterWrong0 implements Counter { - private int c; - - public CounterWrong0() { - c = 0; - } - - @Override - public int incrementAndGet() { -// c++; -// return c; - return ++c; - } -} diff --git a/libtest/src/main/java/tests/custom/counter/CounterWrong1.java b/libtest/src/main/java/tests/custom/counter/CounterWrong1.java deleted file mode 100644 index f279b3abb..000000000 --- a/libtest/src/main/java/tests/custom/counter/CounterWrong1.java +++ /dev/null @@ -1,37 +0,0 @@ -package tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterWrong1 implements Counter { - private int c; - - public CounterWrong1() { - c = 0; - } - - @Override - public int incrementAndGet() { - c++; - return c; - } -} diff --git a/libtest/src/main/java/tests/custom/counter/CounterWrong2.java b/libtest/src/main/java/tests/custom/counter/CounterWrong2.java deleted file mode 100644 index 4b91b3c32..000000000 --- a/libtest/src/main/java/tests/custom/counter/CounterWrong2.java +++ /dev/null @@ -1,36 +0,0 @@ -package tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterWrong2 implements Counter { - private int c; - - public CounterWrong2() { - c = 0; - } - - @Override - public int incrementAndGet() { - return ++c; - } -} diff --git a/libtest/src/main/java/tests/custom/queue/Queue.java b/libtest/src/main/java/tests/custom/queue/Queue.java deleted file mode 100644 index 19b53810a..000000000 --- a/libtest/src/main/java/tests/custom/queue/Queue.java +++ /dev/null @@ -1,28 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public interface Queue { - public void put(int x) throws QueueFullException; - public int get() throws QueueEmptyException; -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueEmptyException.java b/libtest/src/main/java/tests/custom/queue/QueueEmptyException.java deleted file mode 100644 index 4510bf2ba..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueEmptyException.java +++ /dev/null @@ -1,33 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class QueueEmptyException extends Exception { - public QueueEmptyException(String message) { - super(message); - } - - public QueueEmptyException() { - - } -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueFullException.java b/libtest/src/main/java/tests/custom/queue/QueueFullException.java deleted file mode 100644 index 019561020..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueFullException.java +++ /dev/null @@ -1,33 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class QueueFullException extends Exception { - public QueueFullException(String message) { - super(message); - } - - public QueueFullException() { - - } -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueSynchronized.java b/libtest/src/main/java/tests/custom/queue/QueueSynchronized.java deleted file mode 100644 index 7eb34acbb..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueSynchronized.java +++ /dev/null @@ -1,77 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.Arrays; - -public class QueueSynchronized implements Queue { - private int indGet; - private int indPut; - private int countElements; - - private int[] items; - - private int inc(int i) { - return (++i == items.length ? 0 : i); - } - - public QueueSynchronized(int capacity) { - items = new int[capacity]; - - indPut = 0; - indGet = 0; - countElements = 0; - - } - - @Override - public synchronized void put(int x) throws QueueFullException { - if (countElements == items.length) { - throw new QueueFullException(); - } - items[indPut] = x; - indPut = inc(indPut); - countElements++; - } - - @Override - public synchronized int get() throws QueueEmptyException { - if (countElements == 0) { - throw new QueueEmptyException(); - } - int ret = items[indGet]; - indGet = inc(indGet); - countElements--; - return ret; - } - - @Override - public String toString() { - return "QueueWithoutAnySync{" + - "indGet=" + indGet + - ", indPut=" + indPut + - ", countElements=" + countElements + - ", items=" + Arrays.toString(items) + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueWrong1.java b/libtest/src/main/java/tests/custom/queue/QueueWrong1.java deleted file mode 100644 index f545f67c2..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueWrong1.java +++ /dev/null @@ -1,77 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.Arrays; - -public class QueueWrong1 implements Queue { - private int indGet; - private int indPut; - private int countElements; - - private int[] items; - - private int inc(int i) { - return (++i == items.length ? 0 : i); - } - - public QueueWrong1(int capacity) { - items = new int[capacity]; - - indPut = 0; - indGet = 0; - countElements = 0; - - } - - @Override - public void put(int x) throws QueueFullException { - if (countElements == items.length) { - throw new QueueFullException(); - } - items[indPut] = x; - indPut = inc(indPut); - countElements++; - } - - @Override - public int get() throws QueueEmptyException { - if (countElements == 0) { - throw new QueueEmptyException(); - } - int ret = items[indGet]; - indGet = inc(indGet); - countElements--; - return ret; - } - - @Override - public String toString() { - return "QueueWithoutAnySync{" + - "indGet=" + indGet + - ", indPut=" + indPut + - ", countElements=" + countElements + - ", items=" + Arrays.toString(items) + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueWrong2.java b/libtest/src/main/java/tests/custom/queue/QueueWrong2.java deleted file mode 100644 index 030e40103..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueWrong2.java +++ /dev/null @@ -1,77 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.Arrays; - -public class QueueWrong2 implements Queue { - private int indGet; - private int indPut; - private int countElements; - - private int[] items; - - private int inc(int i) { - return (++i == items.length ? 0 : i); - } - - public QueueWrong2(int capacity) { - items = new int[capacity]; - - indPut = 0; - indGet = 0; - countElements = 0; - - } - - @Override - public synchronized void put(int x) throws QueueFullException { - if (countElements == items.length) { - throw new QueueFullException(); - } - items[indPut] = x; - indPut = inc(indPut); - countElements++; - } - - @Override - public int get() throws QueueEmptyException { - if (countElements == 0) { - throw new QueueEmptyException(); - } - int ret = items[indGet]; - indGet = inc(indGet); - countElements--; - return ret; - } - - @Override - public String toString() { - return "QueueWithoutAnySync{" + - "indGet=" + indGet + - ", indPut=" + indPut + - ", countElements=" + countElements + - ", items=" + Arrays.toString(items) + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/queue/QueueWrong3.java b/libtest/src/main/java/tests/custom/queue/QueueWrong3.java deleted file mode 100644 index 5df308cb7..000000000 --- a/libtest/src/main/java/tests/custom/queue/QueueWrong3.java +++ /dev/null @@ -1,77 +0,0 @@ -package tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.Arrays; - -public class QueueWrong3 implements Queue { - private int indGet; - private int indPut; - private int countElements; - - private int[] items; - - private int inc(int i) { - return (++i == items.length ? 0 : i); - } - - public QueueWrong3(int capacity) { - items = new int[capacity]; - - indPut = 0; - indGet = 0; - countElements = 0; - - } - - @Override - public void put(int x) throws QueueFullException { - if (countElements == items.length) { - throw new QueueFullException(); - } - items[indPut] = x; - indPut = inc(indPut); - countElements++; - } - - @Override - public synchronized int get() throws QueueEmptyException { - if (countElements == 0) { - throw new QueueEmptyException(); - } - int ret = items[indGet]; - indGet = inc(indGet); - countElements--; - return ret; - } - - @Override - public String toString() { - return "QueueWithoutAnySync{" + - "indGet=" + indGet + - ", indPut=" + indPut + - ", countElements=" + countElements + - ", items=" + Arrays.toString(items) + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/transfer/Accounts.java b/libtest/src/main/java/tests/custom/transfer/Accounts.java deleted file mode 100644 index 73f118691..000000000 --- a/libtest/src/main/java/tests/custom/transfer/Accounts.java +++ /dev/null @@ -1,29 +0,0 @@ -package tests.custom.transfer; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public interface Accounts { - public Integer getAmount(int id); - public void setAmount(int id, int value); - public void transfer(int id1, int id2, int value); -} diff --git a/libtest/src/main/java/tests/custom/transfer/AccountsWrong1.java b/libtest/src/main/java/tests/custom/transfer/AccountsWrong1.java deleted file mode 100644 index 66bc5be74..000000000 --- a/libtest/src/main/java/tests/custom/transfer/AccountsWrong1.java +++ /dev/null @@ -1,74 +0,0 @@ -package tests.custom.transfer; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.HashMap; -import java.util.Map; - -public class AccountsWrong1 implements Accounts { - - Map data; - - public AccountsWrong1() { - data = new HashMap<>(); - } - - @Override - public Integer getAmount(int id) { - if (data.containsKey(id)) { - return data.get(id); - } else { - return 0; - } - } - - @Override - public void setAmount(int id, int value) { - data.put(id, value); - } - - @Override - public synchronized void transfer(int id1, int id2, int value) { - if (id1 == id2) return; - Integer v1 = data.get(id1); - Integer v2 = data.get(id2); - if (v1 == null) v1 = 0; - if (v2 == null) v2 = 0; - v1 -= value; - v2 += value; - data.put(id1, v1); -// try { -// Thread.sleep(10); -// } catch (InterruptedException e) { -// e.printStackTrace(); -// } - data.put(id2, v2); - } - - @Override - public String toString() { - return "AccountsSynchronized{" + - "data=" + data + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/transfer/AccountsWrong2.java b/libtest/src/main/java/tests/custom/transfer/AccountsWrong2.java deleted file mode 100644 index 7479f8357..000000000 --- a/libtest/src/main/java/tests/custom/transfer/AccountsWrong2.java +++ /dev/null @@ -1,74 +0,0 @@ -package tests.custom.transfer; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.HashMap; -import java.util.Map; - -public class AccountsWrong2 implements Accounts { - - Map data; - - public AccountsWrong2() { - data = new HashMap<>(); - } - - @Override - public Integer getAmount(int id) { - if (data.containsKey(id)) { - return data.get(id); - } else { - return 0; - } - } - - @Override - public synchronized void setAmount(int id, int value) { - data.put(id, value); - } - - @Override - public void transfer(int id1, int id2, int value) { - if (id1 == id2) return; - Integer v1 = data.get(id1); - Integer v2 = data.get(id2); - if (v1 == null) v1 = 0; - if (v2 == null) v2 = 0; - v1 -= value; - v2 += value; - data.put(id1, v1); -// try { -// Thread.sleep(10); -// } catch (InterruptedException e) { -// e.printStackTrace(); -// } - data.put(id2, v2); - } - - @Override - public String toString() { - return "AccountsSynchronized{" + - "data=" + data + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/transfer/AccountsWrong3.java b/libtest/src/main/java/tests/custom/transfer/AccountsWrong3.java deleted file mode 100644 index 52a09685a..000000000 --- a/libtest/src/main/java/tests/custom/transfer/AccountsWrong3.java +++ /dev/null @@ -1,74 +0,0 @@ -package tests.custom.transfer; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.HashMap; -import java.util.Map; - -public class AccountsWrong3 implements Accounts { - - Map data; - - public AccountsWrong3() { - data = new HashMap<>(); - } - - @Override - public Integer getAmount(int id) { - if (data.containsKey(id)) { - return data.get(id); - } else { - return 0; - } - } - - @Override - public void setAmount(int id, int value) { - data.put(id, value); - } - - @Override - public void transfer(int id1, int id2, int value) { - if (id1 == id2) return; - Integer v1 = data.get(id1); - Integer v2 = data.get(id2); - if (v1 == null) v1 = 0; - if (v2 == null) v2 = 0; - v1 -= value; - v2 += value; - data.put(id1, v1); -// try { -// Thread.sleep(10); -// } catch (InterruptedException e) { -// e.printStackTrace(); -// } - data.put(id2, v2); - } - - @Override - public String toString() { - return "AccountsSynchronized{" + - "data=" + data + - '}'; - } -} diff --git a/libtest/src/main/java/tests/custom/transfer/AccountsWrong4.java b/libtest/src/main/java/tests/custom/transfer/AccountsWrong4.java deleted file mode 100644 index 02ee9ac98..000000000 --- a/libtest/src/main/java/tests/custom/transfer/AccountsWrong4.java +++ /dev/null @@ -1,66 +0,0 @@ -package tests.custom.transfer; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import java.util.HashMap; -import java.util.Map; - -public class AccountsWrong4 implements Accounts { - - Map data; - - public AccountsWrong4() { - data = new HashMap<>(1); - } - - // This operation is not synchronized with others - @Override - public Integer getAmount(int id) { - return data.getOrDefault(id, 0); - } - - @Override - public synchronized void setAmount(int id, int value) { - data.put(id, value); - } - - @Override - public synchronized void transfer(int id1, int id2, int value) { - if (id1 == id2) return; - Integer v1 = data.get(id1); - Integer v2 = data.get(id2); - if (v1 == null) v1 = 0; - if (v2 == null) v2 = 0; - v1 -= value; - v2 += value; - data.put(id1, v1); - data.put(id2, v2); - } - - @Override - public String toString() { - return "AccountsSynchronized{" + - "data=" + data + - '}'; - } -} diff --git a/libtest/src/main/java/thesis_example/Counter.java b/libtest/src/main/java/thesis_example/Counter.java deleted file mode 100644 index e1315ba40..000000000 --- a/libtest/src/main/java/thesis_example/Counter.java +++ /dev/null @@ -1,27 +0,0 @@ -package thesis_example; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public interface Counter { - public int incrementAndGet(); -} \ No newline at end of file diff --git a/libtest/src/main/java/thesis_example/CounterCorrect1.java b/libtest/src/main/java/thesis_example/CounterCorrect1.java deleted file mode 100644 index 58f326e7b..000000000 --- a/libtest/src/main/java/thesis_example/CounterCorrect1.java +++ /dev/null @@ -1,36 +0,0 @@ -package thesis_example; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterCorrect1 { - private int c = 0; - - public synchronized int incrementAndGet() { - c++; - return c; - } - - public static void main(String[] args) { - System.out.println(new CounterCorrect1().incrementAndGet()); - } -} diff --git a/libtest/src/main/java/thesis_example/CounterWrong1.java b/libtest/src/main/java/thesis_example/CounterWrong1.java deleted file mode 100644 index c10961c76..000000000 --- a/libtest/src/main/java/thesis_example/CounterWrong1.java +++ /dev/null @@ -1,37 +0,0 @@ -package thesis_example; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterWrong1 implements Counter { - private int c; - - public CounterWrong1() { - c = 0; - } - - @Override - public int incrementAndGet() { - c++; - return c; - } -} diff --git a/libtest/src/main/java/thesis_example/CounterWrong2.java b/libtest/src/main/java/thesis_example/CounterWrong2.java deleted file mode 100644 index af3175375..000000000 --- a/libtest/src/main/java/thesis_example/CounterWrong2.java +++ /dev/null @@ -1,36 +0,0 @@ -package thesis_example; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -public class CounterWrong2 implements Counter { - private int c; - - public CounterWrong2() { - c = 0; - } - - @Override - public int incrementAndGet() { - return ++c; - } -} diff --git a/libtest/src/main/java/thesis_example/QueueCorrect.java b/libtest/src/main/java/thesis_example/QueueCorrect.java deleted file mode 100644 index 09f27d0d1..000000000 --- a/libtest/src/main/java/thesis_example/QueueCorrect.java +++ /dev/null @@ -1,66 +0,0 @@ -package thesis_example; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import tests.custom.queue.QueueEmptyException; -import tests.custom.queue.QueueFullException; - -public class QueueCorrect { - private int indGet; - private int indPut; - private int countElements; - - private int[] items; - - private int inc(int i) { - return (++i == items.length ? 0 : i); - } - - public QueueCorrect(int capacity) { - items = new int[capacity]; - - indPut = 0; - indGet = 0; - countElements = 0; - - } - - public synchronized void put(int x) throws QueueFullException { - if (countElements == items.length) { - throw new QueueFullException(); - } - items[indPut] = x; - indPut = inc(indPut); - countElements++; - } - - public synchronized int get() throws QueueEmptyException { - if (countElements == 0) { - throw new QueueEmptyException(); - } - int ret = items[indGet]; - indGet = inc(indGet); - countElements--; - return ret; - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrect1.java deleted file mode 100644 index c473f19c9..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrect1.java +++ /dev/null @@ -1,54 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.boundary; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.cliffc.high_scale_lib.NonBlockingSetInt; -import org.junit.Test; - -import java.util.Set; - -@StressCTest -@Param(name = "key", gen = IntGen.class, conf = "1:10") -public class BitVectorCorrect1 { - private Set q = new NonBlockingSetInt(); - - @Operation(params = {"key"}) - public boolean add(int key) { - return q.add(key); - } - - @Operation - public boolean remove(@Param(name = "key") int key) { - return q.remove(key); - } - - @Test - public void test() { - LinChecker.check(BitVectorCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrectTest.kt similarity index 53% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest1.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrectTest.kt index 2dc567c2d..ccdbdc965 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest1.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/BitVectorCorrectTest.kt @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.counter; - /* * #%L * libtest @@ -10,36 +8,34 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.tests.boundary + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.cliffc.high_scale_lib.NonBlockingSetInt +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.counter.Counter; -import tests.custom.counter.CounterWrong0; +@Param(name = "key", gen = IntGen::class, conf = "1:10") +class BitVectorCorrectTest : AbstractLinCheckTest() { + private val q = NonBlockingSetInt() -@StressCTest -public class CounterTest1 { - private Counter counter = new CounterWrong0(); + @Operation(params = ["key"]) + fun add(key: Int): Boolean = q.add(key) @Operation - public int incAndGet() { - return counter.incrementAndGet(); - } + fun remove(@Param(name = "key") key: Int): Boolean = q.remove(key) - @Test(expected = AssertionError.class) - public void test() { - LinChecker.check(CounterTest1.class); - } + public override fun extractState(): Any = q } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrect1.java deleted file mode 100644 index 9ce42e2f3..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrect1.java +++ /dev/null @@ -1,60 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.boundary; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.cliffc.high_scale_lib.NonBlockingHashMap; -import org.junit.Test; - -import java.util.Map; - -@StressCTest -@Param(name = "key", gen = IntGen.class) -@Param(name = "value", gen = IntGen.class) -public class MapCorrect1 { - private Map map = new NonBlockingHashMap<>(); - - @Operation - public Integer put(Integer key, Integer value) { - return map.put(key, value); - } - - @Operation - public Integer get(Integer key) { - return map.get(key); - } - - @Operation(handleExceptionsAsResult = NullPointerException.class) - public int putIfAbsent(int key, int value) { - return map.putIfAbsent(key, value); - } - - @Test - public void test() { - LinChecker.check(MapCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest2.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrectTest.kt similarity index 56% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest2.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrectTest.kt index dba25915f..42ff7e53d 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest2.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/MapCorrectTest.kt @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.counter; - /* * #%L * libtest @@ -10,36 +8,34 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.tests.boundary + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.cliffc.high_scale_lib.NonBlockingHashMap +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.counter.Counter; -import tests.custom.counter.CounterCorrect2; +class MapCorrectTest : AbstractLinCheckTest() { + private val map = NonBlockingHashMap() -@StressCTest -public class CounterTest2 { - private Counter counter = new CounterCorrect2(); + @Operation + fun put(key: Int?, value: Int?): Int? = map.put(key, value) + + @Operation + operator fun get(key: Int?): Int? = map[key] @Operation - public int incAndGet() { - return counter.incrementAndGet(); - } + fun putIfAbsent(key: Int, value: Int): Int? = map.putIfAbsent(key, value) - @Test - public void test() { - LinChecker.check(CounterTest2.class); - } + override fun extractState(): Any = map } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrect1.java deleted file mode 100644 index 8cc09c42c..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrect1.java +++ /dev/null @@ -1,52 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.boundary; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.cliffc.high_scale_lib.NonBlockingHashSet; -import org.junit.Test; - -@StressCTest -@Param(name = "key", gen = IntGen.class) -public class SetCorrect1 { - private NonBlockingHashSet q = new NonBlockingHashSet<>(); - - @Operation(params = {"key"}) - public boolean add(int key) { - return q.add(key); - } - - @Operation(params = {"key"}) - public boolean remove(int key) { - return q.remove(key); - } - - @Test - public void test() { - LinChecker.check(SetCorrect1.class); - } -} diff --git a/libtest/src/main/java/thesis_example/CounterCorrect2.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrectTest.kt similarity index 53% rename from libtest/src/main/java/thesis_example/CounterCorrect2.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrectTest.kt index c0d043a17..3557e98ba 100644 --- a/libtest/src/main/java/thesis_example/CounterCorrect2.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/boundary/SetCorrectTest.kt @@ -1,5 +1,3 @@ -package thesis_example; - /* * #%L * libtest @@ -10,30 +8,35 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ -import java.util.concurrent.atomic.AtomicInteger; +package org.jetbrains.kotlinx.lincheck.tests.boundary + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.cliffc.high_scale_lib.NonBlockingHashSet +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +@Param(name = "key", gen = IntGen::class) +class SetCorrectTest : AbstractLinCheckTest() { + private val q = NonBlockingHashSet() -public class CounterCorrect2 implements Counter { - private AtomicInteger c; + @Operation(params = ["key"]) + fun add(key: Int) = q.add(key) - public CounterCorrect2() { - c = new AtomicInteger(); - } + @Operation(params = ["key"]) + fun remove(key: Int) = q.remove(key) - @Override - public synchronized int incrementAndGet() { - return c.incrementAndGet(); - } + override fun extractState(): Any = q } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/transfer/AccountsTest.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/AccountsTest.java similarity index 73% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/transfer/AccountsTest.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/AccountsTest.java index ada6ec0a9..3efe94a6e 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/transfer/AccountsTest.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/AccountsTest.java @@ -1,4 +1,4 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.transfer; +package org.jetbrains.kotlinx.lincheck.tests.custom; /* * #%L @@ -22,23 +22,18 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; +import org.jetbrains.annotations.*; +import org.jetbrains.kotlinx.lincheck.*; import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import tests.custom.transfer.Accounts; -import tests.custom.transfer.AccountsWrong1; -import tests.custom.transfer.AccountsWrong2; -import tests.custom.transfer.AccountsWrong3; -import tests.custom.transfer.AccountsWrong4; +import org.jetbrains.kotlinx.lincheck.annotations.*; +import org.jetbrains.kotlinx.lincheck.paramgen.*; +import org.jetbrains.kotlinx.lincheck.verifier.*; +import org.junit.*; +import org.junit.runner.*; +import org.junit.runners.*; -import java.util.Arrays; -import java.util.List; -import java.util.function.Supplier; +import java.util.*; +import java.util.function.*; @RunWith(Parameterized.class) public class AccountsTest { @@ -46,7 +41,7 @@ public class AccountsTest { @Parameterized.Parameters(name = "{1}") public static List params() { - return Arrays.asList( + return Arrays.asList( new Object[] {(Supplier) AccountsWrong1::new, "AccountsWrong1"}, new Object[] {(Supplier) AccountsWrong2::new, "AccountsWrong2"}, new Object[] {(Supplier) AccountsWrong3::new, "AccountsWrong3"}, @@ -58,10 +53,9 @@ public AccountsTest(Supplier accountCreator, String desc) { AccountsTest.accountCreator = accountCreator; } - @StressCTest(threads = 3, requireStateEquivalenceImplCheck = false) @Param(name = "id", gen = IntGen.class, conf = "1:4") @Param(name = "amount", gen = IntGen.class) - public static class AccountsLinearizabilityTest { + public static class AccountsLinearizabilityTest extends VerifierState { private Accounts acc = accountCreator.get(); @Operation(params = {"id"}) @@ -80,6 +74,12 @@ public void transfer(@Param(name = "id") int from, @Param(name = "id") int to, { acc.transfer(from, to, amount); } + + @NotNull + @Override + protected Object extractState() { + return acc; + } } @Test(expected = AssertionError.class) diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/CounterTests.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/CounterTests.kt new file mode 100644 index 000000000..51bdcdfcf --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/CounterTests.kt @@ -0,0 +1,40 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.strategy.IncorrectIterationResult +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +import kotlin.reflect.KClass + +abstract class AbstractCounterTest(private val counter: Counter, vararg expectedErrors: KClass) : AbstractLinCheckTest(*expectedErrors) { + @Operation + fun incAndGet(): Int = counter.incrementAndGet() + + override fun extractState(): Any = counter.get() +} + +class CounterCorrectTest : AbstractCounterTest(CounterCorrect()) +class CounterWrong0Test : AbstractCounterTest(CounterWrong0(), IncorrectIterationResult::class) +class CounterWrong1Test : AbstractCounterTest(CounterWrong1(), IncorrectIterationResult::class) +class CounterWrong2Test : AbstractCounterTest(CounterWrong2(), IncorrectIterationResult::class) \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/DeadlockTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/DeadlockTest.kt new file mode 100644 index 000000000..d7b62bfe1 --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/DeadlockTest.kt @@ -0,0 +1,55 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.strategy.DeadlockIterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest + +class DeadlockTest : AbstractLinCheckTest(DeadlockIterationResult::class) { + private var counter = 0 + private var lock1 = Any() + private var lock2 = Any() + + @Operation + fun inc12(): Int { + synchronized(lock1) { + synchronized(lock2) { + return counter++ + } + } + } + + @Operation + fun inc21(): Int { + synchronized(lock2) { + synchronized(lock1) { + return counter++ + } + } + } + + override fun > O.customizeOptions(): O = minimizeFailedScenario(false) + + override fun extractState(): Any = counter +} \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSetTests.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSetTests.kt new file mode 100644 index 000000000..531932594 --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSetTests.kt @@ -0,0 +1,48 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +import kotlin.reflect.KClass + +@Param(name = "key", gen = IntGen::class, conf = "1:5") +abstract class AbstractSetTest(private val set: Set, vararg expectedErrors: KClass) : AbstractLinCheckTest(*expectedErrors) { + @Operation + fun add(@Param(name = "key") key: Int): Boolean = set.add(key) + + @Operation + fun remove(@Param(name = "key") key: Int): Boolean = set.remove(key) + + @Operation + operator fun contains(@Param(name = "key") key: Int): Boolean = set.contains(key) + + override fun extractState(): Any = (1..5).map { set.contains(it) } +} + +class SpinLockSetCorrectTest : AbstractSetTest(SpinLockBasedSet()) +class ReentrantLockSetCorrectTest : AbstractSetTest(ReentrantLockBasedSet()) +class SynchronizedLockSetCorrectTest : AbstractSetTest(SynchronizedBlockBasedSet()) +class SynchronizedMethodSetCorrectTest : AbstractSetTest(SynchronizedMethodBasedSet()) \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDequeTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDequeTest.kt similarity index 63% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDequeTest.kt rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDequeTest.kt index 01b05b624..903663d6c 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/LockFreeDequeTest.kt +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockFreeDequeTest.kt @@ -1,15 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.tests - -import org.jetbrains.kotlinx.lincheck.LinChecker -import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchCTest -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest -import org.junit.Test - -@StressCTest(requireStateEquivalenceImplCheck = false) -class DequeLinearizabilityTest { - private val deque = LockFreeDeque(); - /*- * #%L * libtest @@ -20,23 +8,37 @@ class DequeLinearizabilityTest { * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import org.jetbrains.kotlinx.lincheck.LinChecker +import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.paramgen.* +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest +import org.jetbrains.kotlinx.lincheck.verifier.* +import org.junit.Test + +@StressCTest(iterations = 30) +@Param(name = "value", gen = IntGen::class, conf = "1:3") +class DequeLinearizabilityTest : VerifierState() { + private val deque = LockFreeDeque(); @Operation - fun pushLeft(value: Int) = deque.pushLeft(value) + fun pushLeft(@Param(name = "value") value: Int) = deque.pushLeft(value) @Operation - fun pushRight(value: Int) = deque.pushRight(value) + fun pushRight(@Param(name = "value") value: Int) = deque.pushRight(value) @Operation fun popLeft(): Int? = deque.popLeft() @@ -44,6 +46,15 @@ class DequeLinearizabilityTest { @Operation fun popRight(): Int? = deque.popRight() + override fun extractState(): Any { + val elements = ArrayList() + while (true) { + val x = popLeft() ?: break + elements += x + } + return elements + } + @Test fun test() = LinChecker.check(DequeLinearizabilityTest::class.java) } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/MutexStressTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/MutexStressTest.kt similarity index 59% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/MutexStressTest.kt rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/MutexStressTest.kt index 05b3109e7..6e844e39e 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/MutexStressTest.kt +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/MutexStressTest.kt @@ -19,24 +19,18 @@ * . * #L% */ -package org.jetbrains.kotlinx.lincheck.tests.linearizability - -import kotlinx.coroutines.sync.Mutex -import org.jetbrains.kotlinx.lincheck.LinChecker -import org.jetbrains.kotlinx.lincheck.LoggingLevel -import org.jetbrains.kotlinx.lincheck.annotations.LogLevel -import org.jetbrains.kotlinx.lincheck.annotations.Operation -import org.jetbrains.kotlinx.lincheck.annotations.Param -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState -import org.junit.Test -import java.lang.IllegalStateException +package org.jetbrains.kotlinx.lincheck.tests.custom + +import kotlinx.coroutines.sync.* +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck.paramgen.* +import org.jetbrains.kotlinx.lincheck.test.* +import org.junit.* @Param(name = "value", gen = IntGen::class, conf = "1:5") -@StressCTest(actorsPerThread = 10, threads = 2, invocationsPerIteration = 10000, iterations = 100, actorsBefore = 10, actorsAfter = 0, requireStateEquivalenceImplCheck = false) -class MutexStressTest : VerifierState() { - val mutex = Mutex(true) +class MutexStressTest : AbstractLinCheckTest() { + private val mutex = Mutex(true) @Operation(handleExceptionsAsResult = [IllegalStateException::class]) fun tryLock(e: Int) = mutex.tryLock(e) @@ -50,8 +44,8 @@ class MutexStressTest : VerifierState() { @Operation(handleExceptionsAsResult = [IllegalStateException::class]) fun unlock(e: Int) = mutex.unlock(e) + override fun extractState() = (1..5).map { holdsLock(it) } + @Test fun test() = LinChecker.check(MutexStressTest::class.java) - - override fun extractState() = mutex } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/QueueTests.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/QueueTests.kt new file mode 100644 index 000000000..cf8ba9fb8 --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/QueueTests.kt @@ -0,0 +1,47 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.custom + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.strategy.IncorrectIterationResult +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +import kotlin.reflect.KClass + +abstract class AbstractQueueTest(queueConstructor: (Int) -> Queue, vararg expectedErrors: KClass) : AbstractLinCheckTest(*expectedErrors) { + private val queue = queueConstructor(3) + + @Operation(handleExceptionsAsResult = [Queue.FullQueueException::class]) + fun put(@Param(gen = IntGen::class) args: Int) = queue.put(args) + + @Operation(handleExceptionsAsResult = [Queue.EmptyQueueException::class]) + fun get(): Int = queue.get() + + override fun extractState(): Any = queue +} + +class QueueCorrectTest : AbstractQueueTest(::QueueSynchronized) +class QueueWrong1Test : AbstractQueueTest(::QueueWrong1, IncorrectIterationResult::class) +class QueueWrong2Test : AbstractQueueTest(::QueueWrong2, IncorrectIterationResult::class) +class QueueWrong3Test : AbstractQueueTest(::QueueWrong3, IncorrectIterationResult::class) \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterGetTest.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterGetTest.java deleted file mode 100644 index e27e5d65d..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterGetTest.java +++ /dev/null @@ -1,55 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; -import org.junit.Test; -import tests.custom.counter.CounterGet; - -@StressCTest -public class CounterGetTest extends VerifierState { - private CounterGet counter = new CounterGet();; - - @Operation - public int incAndGet() { - return counter.incrementAndGet(); - } - - @Operation - public int get() { - return counter.get(); - } - - @Test - public void test() { - LinChecker.check(CounterGetTest.class); - } - - @Override - protected Object extractState() { - return counter.get(); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest4.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest4.java deleted file mode 100644 index a243991fe..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest4.java +++ /dev/null @@ -1,45 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.counter; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.counter.Counter; -import tests.custom.counter.CounterWrong2; - -@StressCTest -public class CounterTest4 { - private Counter counter = new CounterWrong2(); - - @Operation - public int incAndGet() { - return counter.incrementAndGet(); - } - - @Test(expected = AssertionError.class) - public void test() { - LinChecker.check(CounterTest4.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueCorrect1.java deleted file mode 100644 index a432af23e..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueCorrect1.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.queue.Queue; -import tests.custom.queue.QueueEmptyException; -import tests.custom.queue.QueueSynchronized; - -@StressCTest -public class WrapperQueueCorrect1 { - private Queue queue = new QueueSynchronized(10);; - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public void put(@Param(gen = IntGen.class)int args) throws Exception { - queue.put(args); - } - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public int get() throws Exception { - return queue.get(); - } - - @Test - public void test() { - LinChecker.check(WrapperQueueCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong1.java deleted file mode 100644 index 7d019fbb5..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong1.java +++ /dev/null @@ -1,52 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.queue.Queue; -import tests.custom.queue.QueueEmptyException; -import tests.custom.queue.QueueWrong1; -@StressCTest -public class WrapperQueueWrong1 { - private Queue queue = new QueueWrong1(10); - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public void put(@Param(gen = IntGen.class)int x) throws Exception { - queue.put(x); - } - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public int get() throws Exception { - return queue.get(); - } - - @Test(expected = AssertionError.class) - public void test() { - LinChecker.check(WrapperQueueWrong1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong2.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong2.java deleted file mode 100644 index 551d2e3f0..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong2.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.queue.Queue; -import tests.custom.queue.QueueEmptyException; -import tests.custom.queue.QueueWrong2; - -@StressCTest -public class WrapperQueueWrong2 { - private Queue queue = new QueueWrong2(10); - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public void put(@Param(gen = IntGen.class)int args) throws Exception { - queue.put(args); - } - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public int get() throws Exception { - return queue.get(); - } - - @Test(expected = AssertionError.class) - public void test() throws Exception { - LinChecker.check(WrapperQueueWrong2.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong3.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong3.java deleted file mode 100644 index d73d61fdb..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/queue/WrapperQueueWrong3.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.queue.Queue; -import tests.custom.queue.QueueEmptyException; -import tests.custom.queue.QueueWrong3; - -@StressCTest(requireStateEquivalenceImplCheck = false) -public class WrapperQueueWrong3 { - private Queue queue = new QueueWrong3(10); - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public void put(@Param(gen = IntGen.class)int args) throws Exception { - queue.put(args); - } - - @Operation(handleExceptionsAsResult = QueueEmptyException.class) - public int get() throws Exception { - return queue.get(); - } - - @Test(expected = AssertionError.class) - public void test() throws Exception { - LinChecker.check(WrapperQueueWrong2.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrect1.java deleted file mode 100644 index 7a80a828c..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrect1.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.guava; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import com.google.common.collect.ConcurrentHashMultiset; -import org.junit.Test; - -@StressCTest -@Param(name = "value", gen = IntGen.class) -@Param(name = "count", gen = IntGen.class, conf = "1:10") -public class MultisetCorrect1 { - private ConcurrentHashMultiset q = ConcurrentHashMultiset.create(); - - @Operation(params = {"value", "count"}) - public int add(int value, int count) { - return q.add(value, count); - } - - @Operation(params = {"value", "count"}) - public int remove(int value, int count) { - return q.remove(value, count); - } - - @Test - public void test() { - LinChecker.check(MultisetCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest3.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrectTest.kt similarity index 51% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest3.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrectTest.kt index f78d9b9ab..747168757 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/custom/counter/CounterTest3.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/MultisetCorrectTest.kt @@ -1,4 +1,4 @@ -package org.jetbrains.kotlinx.lincheck.tests.custom.counter; +package org.jetbrains.kotlinx.lincheck.tests.guava /* * #%L @@ -10,36 +10,33 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import tests.custom.counter.Counter; -import tests.custom.counter.CounterWrong1; +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import com.google.common.collect.ConcurrentHashMultiset +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest -@StressCTest -public class CounterTest3 { - private Counter counter = new CounterWrong1(); +@Param(name = "count", gen = IntGen::class, conf = "1:5") +class MultisetCorrectTest : AbstractLinCheckTest() { + private val q = ConcurrentHashMultiset.create() @Operation - public int incAndGet() { - return counter.incrementAndGet(); - } + fun add(value: Int, @Param(name = "count") count: Int): Int = q.add(value, count) - @Test(expected = AssertionError.class) - public void test() { - LinChecker.check(CounterTest3.class); - } + @Operation + fun remove(value: Int, @Param(name = "count") count: Int): Int = q.remove(value, count) + + override fun extractState(): Any = q } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrect1.java deleted file mode 100644 index e331c0866..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrect1.java +++ /dev/null @@ -1,55 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.guava; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; - -import java.util.Collections; -import java.util.Set; -import java.util.concurrent.ConcurrentHashMap; - -@StressCTest -@Param(name = "key", gen = IntGen.class) -public class SetCorrect1 { - private Set q = Collections.newSetFromMap(new ConcurrentHashMap());; - - @Operation(params = {"key"}) - public boolean add(Integer params) { - return q.add(params); - } - - @Operation(params = {"key"}) - public boolean remove(Integer params) { - return q.remove(params); - } - - @Test - public void test() throws Exception { - LinChecker.check(SetCorrect1.class); - } -} diff --git a/libtest/src/main/java/tests/custom/counter/CounterCorrect2.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrectTest.kt similarity index 50% rename from libtest/src/main/java/tests/custom/counter/CounterCorrect2.java rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrectTest.kt index acccbff7e..2b4e68cad 100644 --- a/libtest/src/main/java/tests/custom/counter/CounterCorrect2.java +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/guava/SetCorrectTest.kt @@ -1,4 +1,4 @@ -package tests.custom.counter; +package org.jetbrains.kotlinx.lincheck.tests.guava /* * #%L @@ -10,29 +10,35 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ -import java.util.concurrent.atomic.AtomicInteger; +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest -public class CounterCorrect2 implements Counter { - private AtomicInteger c; +import java.util.Collections +import java.util.concurrent.ConcurrentHashMap - public CounterCorrect2() { - c = new AtomicInteger(); - } +@Param(name = "key", gen = IntGen::class, conf = "1:5") +class SetCorrectTest : AbstractLinCheckTest() { + private val q = Collections.newSetFromMap(ConcurrentHashMap()) - @Override - public synchronized int incrementAndGet() { - return c.incrementAndGet(); - } + @Operation(params = ["key"]) + fun add(params: Int?): Boolean = q.add(params) + + @Operation(params = ["key"]) + fun remove(params: Int?): Boolean = q.remove(params) + + override fun extractState(): Any = q } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/ConcurrentDequeStressTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/ConcurrentDequeStressTest.kt similarity index 61% rename from libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/ConcurrentDequeStressTest.kt rename to libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/ConcurrentDequeStressTest.kt index 921179189..be796a6df 100644 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/linearizability/ConcurrentDequeStressTest.kt +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/ConcurrentDequeStressTest.kt @@ -19,22 +19,17 @@ * . * #L% */ -package org.jetbrains.kotlinx.lincheck.tests.linearizability +package org.jetbrains.kotlinx.lincheck.tests.juc -import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState -import org.junit.Test -import java.lang.AssertionError -import java.util.concurrent.ConcurrentLinkedDeque +import org.jetbrains.kotlinx.lincheck.paramgen.* +import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.test.* +import java.util.concurrent.* @Param(name = "value", gen = IntGen::class, conf = "1:5") -@StressCTest(actorsPerThread = 10, threads = 2, invocationsPerIteration = 10000, iterations = 10, actorsBefore = 10, actorsAfter = 10) -class ConcurrentDequeStressTest : VerifierState() { - - val deque = ConcurrentLinkedDeque() +class ConcurrentDequeStressTest : AbstractLinCheckTest(IncorrectIterationResult::class) { + private val deque = ConcurrentLinkedDeque() @Operation fun addFirst(e: Int) = deque.addFirst(e) @@ -48,8 +43,5 @@ class ConcurrentDequeStressTest : VerifierState() { @Operation fun pollLast() = deque.pollLast() - @Test(expected = AssertionError::class) - fun test() = LinChecker.check(ConcurrentDequeStressTest::class.java) - override fun extractState() = deque.toList() } diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/HashMapTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/HashMapTest.kt new file mode 100644 index 000000000..2688cd39b --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/HashMapTest.kt @@ -0,0 +1,46 @@ +package org.jetbrains.kotlinx.lincheck.tests.juc + +/* + * #%L + * libtest + * %% + * Copyright (C) 2015 - 2018 Devexperts, LLC + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.strategy.IncorrectIterationResult +import org.jetbrains.kotlinx.lincheck.strategy.UnexpectedExceptionIterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest + +import java.util.HashMap + +@Param(name = "key", gen = IntGen::class) +class HashMapTest : AbstractLinCheckTest(IncorrectIterationResult::class, UnexpectedExceptionIterationResult::class) { + private val m = HashMap() + + @Operation + fun put(key: Int, @Param(name = "key") value: Int): Int? = m.put(key, value) + + @Operation + operator fun get(@Param(name = "key") key: Int?): Int? = m[key] + + override fun extractState(): Any = m +} + diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/blocking_queue/BlockingQueueTest1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/blocking_queue/BlockingQueueTest1.java deleted file mode 100644 index bc80144d7..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/blocking_queue/BlockingQueueTest1.java +++ /dev/null @@ -1,65 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.juc.blocking_queue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; - -import java.util.NoSuchElementException; -import java.util.concurrent.ArrayBlockingQueue; -import java.util.concurrent.BlockingQueue; - -@StressCTest -public class BlockingQueueTest1 { - private BlockingQueue q = new ArrayBlockingQueue<>(10); - - @Operation - public boolean add(@Param(gen = IntGen.class) Integer value) { - return q.add(value); - } - - @Operation(handleExceptionsAsResult = NoSuchElementException.class) - public Integer element() { - return q.element(); - } - - @Operation(handleExceptionsAsResult = NoSuchElementException.class) - public Integer remove() { - return q.remove(); - } - - @Operation(handleExceptionsAsResult = NoSuchElementException.class) - public Integer poll() { - return q.poll(); - } - - @Test - public void test() { - LinChecker.check(BlockingQueueTest1.class); - } -} - diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/hash_map/HashMapTest.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/hash_map/HashMapTest.java deleted file mode 100644 index 9e123cbe4..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/juc/hash_map/HashMapTest.java +++ /dev/null @@ -1,63 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.juc.hash_map; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.annotations.NotNull; -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.jetbrains.kotlinx.lincheck.verifier.VerifierState; -import org.junit.Test; - -import java.util.HashMap; -import java.util.Map; - -@StressCTest -@Param(name = "key", gen = IntGen.class) -@Param(name = "value", gen = IntGen.class) -public class HashMapTest extends VerifierState { - private Map m = new HashMap<>(); - - @Operation(params = {"key", "value"}) - public Integer put(Integer key, Integer value) { - return m.put(key, value); - } - - @Operation - public Integer get(@Param(name = "key") Integer key) { - return m.get(key); - } - - @Test(expected = AssertionError.class) - public void test() throws Exception { - LinChecker.check(HashMapTest.class); - } - - @Override - protected Object extractState() { - return m; - } -} - diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/LockFreeQueueTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/LockFreeQueueTest.kt new file mode 100644 index 000000000..363d82814 --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/LockFreeQueueTest.kt @@ -0,0 +1,53 @@ +/*- + * #%L + * libtest + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.lockfreequeue + +import com.github.lock.free.queue.LockFreeQueue +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.strategy.IncorrectIterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +import java.util.ArrayList + +class LockFreeQueueTest : AbstractLinCheckTest(IncorrectIterationResult::class) { + private val q = LockFreeQueue() + + @Operation + fun add(@Param(gen = IntGen::class) value: Int) { + q.add(value) + } + + @Operation + fun takeOrNull(): Any? { + return q.takeOrNull() + } + + override fun extractState(): Any { + val elements = ArrayList() + while (true) { + val element = q.takeOrNull() ?: break + elements.add(element) + } + return elements + } +} \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/QueueCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/QueueCorrect1.java deleted file mode 100644 index f66f40eaa..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/lockfreequeue/QueueCorrect1.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.lockfreequeue; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import com.github.lock.free.queue.LockFreeQueue; - -/** - * https://github.com/yaitskov/lock-free-queue - */ -@StressCTest -public class QueueCorrect1 { - private LockFreeQueue q = new LockFreeQueue<>(); - - @Operation - public void add(@Param(gen = IntGen.class) int value) { - q.add(value); - } - - @Operation - public Object takeOrNull() { - return q.takeOrNull(); - } - - // @Test TODO is it really correct? - public void test() { - LinChecker.check(QueueCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/romix/TrieCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/romix/TrieCorrect1.java deleted file mode 100644 index 8f3ee1475..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/romix/TrieCorrect1.java +++ /dev/null @@ -1,56 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.romix; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.junit.Test; -import romix.scala.collection.concurrent.TrieMap; - -import java.util.Map; - -@StressCTest -@Param(name = "key", gen = IntGen.class) -@Param(name = "value", gen = IntGen.class) -public class TrieCorrect1 { - private Map m = new TrieMap<>(); - - @Operation(params = {"key", "value"}) - public Integer put(Integer key, Integer value) { - return m.put(key, value); - } - - @Operation(params = {"key"}) - public Integer get(Integer key) { - return m.get(key); - } - - @Test - public void test() { - LinChecker.check(TrieCorrect1.class); - } -} - diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/GenericMPMCQueueTest.kt b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/GenericMPMCQueueTest.kt new file mode 100644 index 000000000..faed8dae0 --- /dev/null +++ b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/GenericMPMCQueueTest.kt @@ -0,0 +1,51 @@ +/*- + * #%L + * libtest + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.tests.zchannel + +import org.jetbrains.kotlinx.lincheck.annotations.Operation +import org.jetbrains.kotlinx.lincheck.annotations.Param +import org.jetbrains.kotlinx.lincheck.paramgen.IntGen +import org.jetbrains.kotlinx.lincheck.strategy.IncorrectIterationResult +import org.jetbrains.kotlinx.lincheck.test.AbstractLinCheckTest +import z.channel.GenericMPMCQueue + +/** + * http://landz.github.io/ + */ +class GenericMPMCQueueTest : AbstractLinCheckTest(IncorrectIterationResult::class) { + private val q = GenericMPMCQueue(4) + + @Operation + fun offer(@Param(gen = IntGen::class) value: Int): Boolean = q.offer(value) + + @Operation + fun poll(): Int? = q.poll() + + override fun extractState(): Any { + val elements = mutableListOf() + while (true) { + val element = q.poll() ?: break + elements.add(element) + } + return elements + } +} \ No newline at end of file diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect1.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect1.java deleted file mode 100644 index f481f76c7..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect1.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.zchannel; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import z.channel.GenericMPMCQueue; - -/** - * http://landz.github.io/ - */ -@StressCTest -public class QueueCorrect1 { - private GenericMPMCQueue q = new GenericMPMCQueue<>(4); - - @Operation - public boolean offer(@Param(gen = IntGen.class) int value) { - return q.offer(value); - } - - @Operation - public Integer poll() { - return q.poll(); - } - -// @Test TODO is it really correct? - public void test() throws Exception { - LinChecker.check(QueueCorrect1.class); - } -} diff --git a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect2.java b/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect2.java deleted file mode 100644 index 4d31482ae..000000000 --- a/libtest/src/test/java/org/jetbrains/kotlinx/lincheck/tests/zchannel/QueueCorrect2.java +++ /dev/null @@ -1,53 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.tests.zchannel; - -/* - * #%L - * libtest - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import z.channel.GenericMPMCQueue; - -/** - * http://landz.github.io/ - */ -@StressCTest -public class QueueCorrect2 { - private GenericMPMCQueue q = new GenericMPMCQueue<>(16); - - @Operation - public boolean offer(@Param(gen = IntGen.class) int value) { - return q.offer(value); - } - - @Operation - public Integer poll() { - return q.poll(); - } - - // @Test TODO is it really correct? - public void test() throws Exception { - LinChecker.check(QueueCorrect2.class); - } -} \ No newline at end of file diff --git a/lincheck/pom.xml b/lincheck/pom.xml index 16cfb6b64..d48e95b17 100755 --- a/lincheck/pom.xml +++ b/lincheck/pom.xml @@ -10,6 +10,22 @@ lincheck Lincheck + + + + org.apache.maven.plugins + maven-jar-plugin + + + + test-jar + + + + + + + org.ow2.asm diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java deleted file mode 100644 index e32a415e7..000000000 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.java +++ /dev/null @@ -1,196 +0,0 @@ -package org.jetbrains.kotlinx.lincheck; - -/* - * #%L - * Lincheck - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.annotations.LogLevel; -import org.jetbrains.kotlinx.lincheck.execution.*; -import org.jetbrains.kotlinx.lincheck.strategy.Strategy; -import org.jetbrains.kotlinx.lincheck.verifier.*; -import static org.jetbrains.kotlinx.lincheck.ReporterKt.DEFAULT_LOG_LEVEL; -import java.util.*; - - -/** - * This class runs concurrent tests. - * See {@link #check(Class)} and {@link #check(Class, Options)} methods for details. - */ -public class LinChecker { - private final Class testClass; - private final List testConfigurations; - private final CTestStructure testStructure; - private final Reporter reporter; - - private LinChecker(Class testClass, Options options) { - this.testClass = testClass; - this.testStructure = CTestStructure.getFromTestClass(testClass); - LoggingLevel logLevel; - if (options != null) { - logLevel = options.logLevel; - this.testConfigurations = Collections.singletonList(options.createTestConfigurations(testClass)); - } else { - logLevel = getLogLevelFromAnnotation(); - this.testConfigurations = CTestConfiguration.createFromTestClass(testClass); - } - this.reporter = new Reporter(logLevel); - } - - /** - * Runs all concurrent tests described with {@code @CTest} annotations on the specified test class. - * - * @throws AssertionError if algorithm or data structure is not correct. - */ - public static void check(Class testClass) { - check(testClass, null); - } - - /** - * Runs concurrent test on specified class with the specified by options environment. - *

- * NOTE: this method ignores {@code @CTest} annotations on the test class. - * - * @throws AssertionError if algorithm or data structure is not correct. - */ - public static void check(Class testClass, Options options) { - new LinChecker(testClass, options).check(); - } - - /** - * @throws AssertionError if algorithm or data structure is not correct - */ - private void check() throws AssertionError { - if (testConfigurations.isEmpty()) { - throw new IllegalStateException("No Lin-Check test configuration to run"); - } - testConfigurations.forEach(testConfiguration -> { - try { - checkImpl(testConfiguration); - } catch (RuntimeException | AssertionError e) { - throw e; - } catch (Exception e) { - throw new IllegalStateException(e); - } - }); - } - - private void checkImpl(CTestConfiguration testCfg) throws AssertionError, Exception { - ExecutionGenerator exGen = createExecutionGenerator(testCfg.generatorClass, testCfg); - // Run iterations - for (int iteration = 1; iteration <= testCfg.iterations; iteration++) { - ExecutionScenario scenario = exGen.nextExecution(); - // Check correctness of the generated scenario - reporter.logIteration(iteration, testCfg.iterations, scenario); - try { - runScenario(scenario, testCfg); - } catch (AssertionError e) { - if (!testCfg.minimizeFailedScenario) throw e; - minimizeScenario(scenario, testCfg, e); - } - } - } - - // Tries to minimize the specified failing scenario to make the error easier to understand. - // The algorithm is greedy: it tries to remove one actor from the scenario and checks - // whether a test with the modified one fails with error as well. If it fails, - // then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively. - // Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed. - // Thus, the algorithm works in the linear time of the total number of actors. - private void minimizeScenario(ExecutionScenario scenario, CTestConfiguration testCfg, AssertionError currentError) throws AssertionError, Exception { - reporter.logScenarioMinimization(scenario); - for (int i = 0; i < scenario.parallelExecution.size(); i++) { - for (int j = 0; j < scenario.parallelExecution.get(i).size(); j++) { - ExecutionScenario newScenario = copyScenario(scenario); - newScenario.parallelExecution.get(i).remove(j); - if (newScenario.parallelExecution.get(i).isEmpty()) - newScenario.parallelExecution.remove(i); // remove empty thread - minimizeNewScenarioAttempt(newScenario, testCfg); - } - } - for (int i = 0; i < scenario.initExecution.size(); i++) { - ExecutionScenario newScenario = copyScenario(scenario); - newScenario.initExecution.remove(i); - minimizeNewScenarioAttempt(newScenario, testCfg); - } - for (int i = 0; i < scenario.postExecution.size(); i++) { - ExecutionScenario newScenario = copyScenario(scenario); - newScenario.postExecution.remove(i); - minimizeNewScenarioAttempt(newScenario, testCfg); - } - throw currentError; - } - - private void minimizeNewScenarioAttempt(ExecutionScenario newScenario, CTestConfiguration testCfg) throws AssertionError, Exception { - try { - runScenario(newScenario, testCfg); - } catch (IllegalArgumentException e) { - // Ignore incorrect scenarios - } catch (AssertionError e) { - // Scenario has been minimized! Try to minimize more! - minimizeScenario(newScenario, testCfg, e); - throw new IllegalStateException("Never reaches, the previous `minimizeScenario` call always throw an exception"); - } - } - - private ExecutionScenario copyScenario(ExecutionScenario scenario) { - List initExecution = new ArrayList<>(scenario.initExecution); - List> parallelExecution = new ArrayList<>(); - for (int i = 0; i < scenario.parallelExecution.size(); i++) { - parallelExecution.add(new ArrayList<>(scenario.parallelExecution.get(i))); - } - List postExecution = new ArrayList<>(scenario.postExecution); - return new ExecutionScenario(initExecution, parallelExecution, postExecution); - } - - private void runScenario(ExecutionScenario scenario, CTestConfiguration testCfg) throws AssertionError, Exception { - validateScenario(testCfg, scenario); - Verifier verifier = createVerifier(testCfg.verifierClass, scenario, testCfg.sequentialSpecification); - if (testCfg.requireStateEquivalenceImplCheck) verifier.checkStateEquivalenceImplementation(); - Strategy strategy = Strategy.createStrategy(testCfg, testClass, scenario, verifier, reporter); - strategy.run(); - } - - private void validateScenario(CTestConfiguration testCfg, ExecutionScenario scenario) { - if (scenario.hasSuspendableActors()) { - if (scenario.initExecution.stream().anyMatch(Actor::isSuspendable)) - throw new IllegalArgumentException("Generated execution scenario for the test class with suspendable methods contains suspendable actors in initial part"); - if (scenario.parallelExecution.stream().anyMatch(actors -> actors.stream().anyMatch(Actor::isSuspendable)) && scenario.postExecution.size() > 0) - throw new IllegalArgumentException("Generated execution scenario for the test class with suspendable methods has non-empty post part"); - } - } - - private Verifier createVerifier(Class verifierClass, ExecutionScenario scenario, - Class sequentialSpecification) throws Exception { - return verifierClass.getConstructor(ExecutionScenario.class, Class.class).newInstance(scenario, sequentialSpecification); - } - - private ExecutionGenerator createExecutionGenerator(Class generatorClass, - CTestConfiguration testConfiguration) throws Exception { - return generatorClass.getConstructor(CTestConfiguration.class, CTestStructure.class).newInstance(testConfiguration, testStructure); - } - - private LoggingLevel getLogLevelFromAnnotation() { - LogLevel logLevelAnn = testClass.getAnnotation(LogLevel.class); - if (logLevelAnn == null) - return DEFAULT_LOG_LEVEL; - return logLevelAnn.value(); - } -} \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.kt new file mode 100644 index 000000000..daba1ec0e --- /dev/null +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/LinChecker.kt @@ -0,0 +1,197 @@ +/* + * #%L + * Lincheck + * %% + * Copyright (C) 2015 - 2018 Devexperts, LLC + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck + +import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.runner.* +import org.jetbrains.kotlinx.lincheck.strategy.* +import org.jetbrains.kotlinx.lincheck.verifier.* +import java.util.* + +/** + * This class runs concurrent tests. + * See [.check] and [.check] methods for details. + */ +private class LinChecker (private val testClass: Class<*>, options: Options<*, *>?) { + private val testConfigurations: List + private val testStructure: CTestStructure + private val reporter: Reporter + /** + * @throws AssertionError if algorithm or data structure is not correct + */ + @Throws(AssertionError::class) + fun check() { + val resultsByConfiguration = checkDetailed() + for (results in resultsByConfiguration.values) { + val lastResult = results[results.size - 1] + if (lastResult.isError) throw AssertionError(reporter.generateReport(lastResult)) + } + } + + init { + testStructure = CTestStructure.getFromTestClass(testClass) + val logLevel: LoggingLevel + if (options != null) { + logLevel = options.logLevel + testConfigurations = listOf(options.createTestConfigurations(testClass)) + } else { + logLevel = logLevelFromAnnotation + testConfigurations = CTestConfiguration.createFromTestClass(testClass) + } + reporter = Reporter(logLevel) + } + + /** + * @return TestReport with information about concurrent test run. + */ + @Throws(AssertionError::class) + fun checkDetailed(): Map> { + check(!testConfigurations!!.isEmpty()) { "No Lin-Check test configuration to run" } + val resultsByConfiguration: MutableMap> = HashMap() + for (testConfiguration in testConfigurations) { + try { + val results: List = checkDetailedImpl(testConfiguration) + resultsByConfiguration[testConfiguration] = results + if (results[results.size - 1].isError) return resultsByConfiguration + } catch (e: Exception) { // an Exception in LinCheck + throw IllegalStateException(e) + } + } + return resultsByConfiguration + } + + /** + * Generates the specified in the configuration number of scenarios, invokes them, + * and returns the corresponding invocation results. + */ + @Throws(Exception::class) + private fun generateScenariosAndInvoke(testCfg: CTestConfiguration): Map> { + val exGen = createExecutionGenerator(testCfg.generatorClass, testCfg) + val allResults: MutableMap> = HashMap() + // Run iterations + for (iteration in 1..testCfg.iterations) { + val scenario = exGen.nextExecution() + validateScenario(scenario) + val strategy = Strategy.createStrategy(testCfg, testClass, scenario, reporter) + val scenarioResults = strategy.run() + allResults[scenario] = scenarioResults + // Check whether an error is already detected + if (scenarioResults.stream().anyMatch(InvocationResult::isError)) break + } + return allResults + } + + // Tries to minimize the specified failing scenario to make the error easier to understand. +// The algorithm is greedy: it tries to remove one actor from the scenario and checks +// whether a test with the modified one fails with error as well. If it fails, +// then the scenario has been successfully minimized, and the algorithm tries to minimize it again, recursively. +// Otherwise, if no actor can be removed so that the generated test fails, the minimization is completed. +// Thus, the algorithm works in the linear time of the total number of actors. + @Throws(AssertionError::class, Exception::class) + private fun minimizeScenario(scenario: ExecutionScenario, testCfg: CTestConfiguration, currentReport: IterationResult): IterationResult { + reporter.logScenarioMinimization(scenario) + for (i in scenario.parallelExecution.indices) { + for (j in scenario.parallelExecution[i].indices) { + val newScenario = copyScenario(scenario) + newScenario.parallelExecution[i].removeAt(j) + if (newScenario.parallelExecution[i].isEmpty()) newScenario.parallelExecution.removeAt(i) // remove empty thread + val result = minimizeNewScenarioAttempt(newScenario, testCfg) + if (result.isError) return result + } + } + for (i in scenario.initExecution.indices) { + val newScenario = copyScenario(scenario) + newScenario.initExecution.removeAt(i) + val result = minimizeNewScenarioAttempt(newScenario, testCfg) + if (result.isError) return result + } + for (i in scenario.postExecution.indices) { + val newScenario = copyScenario(scenario) + newScenario.postExecution.removeAt(i) + val result = minimizeNewScenarioAttempt(newScenario, testCfg) + if (result.isError) return result + } + return currentReport + } + + @Throws(AssertionError::class, Exception::class) + private fun minimizeNewScenarioAttempt(newScenario: ExecutionScenario, testCfg: CTestConfiguration): IterationResult { + try { + val result: IterationResult = runScenario(newScenario, testCfg) + if (result.isError) return minimizeScenario(newScenario, testCfg, result) + } catch (e: IllegalArgumentException) { // Ignore incorrect scenarios + } + return SuccessIterationResult(newScenario, testCfg.iterations) + } + + private fun copyScenario(scenario: ExecutionScenario): ExecutionScenario { + val initExecution: List = ArrayList(scenario.initExecution) + val parallelExecution: MutableList> = ArrayList() + for (i in scenario.parallelExecution.indices) { + parallelExecution.add(ArrayList(scenario.parallelExecution[i])) + } + val postExecution: List = ArrayList(scenario.postExecution) + return ExecutionScenario(initExecution, parallelExecution, postExecution) + } + + private fun validateScenario(scenario: ExecutionScenario) { + if (scenario.hasSuspendableActors()) { + require(!scenario.initExecution.stream().anyMatch(Actor::isSuspendable)) { "Generated execution scenario for the test class with suspendable methods contains suspendable actors in initial part" } + require(!(scenario.parallelExecution.stream().anyMatch { actors: List -> actors.stream().anyMatch(Actor::isSuspendable) } && scenario.postExecution.size > 0)) { "Generated execution scenario for the test class with suspendable methods has non-empty post part" } + } + } + + private fun createVerifier(verifierClass: Class, scenario: ExecutionScenario, sequentialSpecification: Class<*>) = + verifierClass.getConstructor(ExecutionScenario::class.java, Class::class.java).newInstance(scenario, sequentialSpecification) + + private fun createExecutionGenerator(generatorClass: Class, testConfiguration: CTestConfiguration) = + generatorClass.getConstructor(CTestConfiguration::class.java, CTestStructure::class.java).newInstance(testConfiguration, testStructure) + + private val logLevelFromAnnotation = testClass.getAnnotation(LogLevel::class.java)?.value ?: DEFAULT_LOG_LEVEL + + // We use this companion object for backwards compatibility. + companion object { + /** + * Runs the specified concurrent tests. If [options] is null, the provided on + * the testing class `@...CTest` annotations are used to specify the test parameters. + * + * @throws AssertionError if any of the tests fails. + */ + @JvmStatic + @JvmOverloads + fun ?> check(testClass: Class<*>, options: O? = null) { + LinChecker(testClass, options).check() + } + } +} + + +/** + * This is a short-cut for the following code: + * ``` + * val options = ... + * LinChecker.check(testClass, options) + * ``` + */ +fun > O.check(testClass: Class<*>) = LinChecker.check(testClass, this) \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java index 0a5faafb5..e1b7e34e7 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Options.java @@ -164,5 +164,4 @@ public OPT sequentialSpecification(Class clazz) { this.sequentialSpecification = clazz; return (OPT) this; } - } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Reporter.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Reporter.kt index f6a6b4f5f..ac93f8fbb 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Reporter.kt +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/Reporter.kt @@ -3,6 +3,7 @@ * Lincheck * %% * Copyright (C) 2015 - 2018 Devexperts, LLC + * Copyright (C) 2019 JetBrains s.r.o. * %% * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as @@ -19,12 +20,11 @@ * . * #L% */ - package org.jetbrains.kotlinx.lincheck -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario -import java.io.PrintStream +import org.jetbrains.kotlinx.lincheck.execution.* +import org.jetbrains.kotlinx.lincheck.runner.* +import java.io.* class Reporter @JvmOverloads constructor(val logLevel: LoggingLevel, val out: PrintStream = System.out) { fun logIteration(iteration: Int, maxIterations: Int, scenario: ExecutionScenario) = synchronized(this) { @@ -43,6 +43,36 @@ class Reporter @JvmOverloads constructor(val logLevel: LoggingLevel, val out: Pr } } + fun generateReport(result: IterationResult): String = StringBuilder().apply { + when (result) { + is IncorrectIterationResult -> { + appendln("Incorrect interleaving found:") + appendIncorrectResults(result.scenario, result.results) + } + is UnexpectedExceptionIterationResult -> { + appendln("Illegal exception was thrown:") + appendExecutionScenario(result.scenario) + appendln() + appendExceptionStackTrace(result.exception) + } + is DeadlockIterationResult -> { + appendln("The execution has hung, see the thread dump:") + for ((t, stackTrace) in result.threadDump) { + t as ParallelThreadsRunner.TestThread + appendln("Thread-${t.iThread}:") + for (ste in stackTrace) { + if (logLevel > LoggingLevel.DEBUG && ste.className.startsWith("org.jetbrains.kotlinx.lincheck.runner.")) break + appendln("\t$ste") + } + appendln() + } + appendExecutionScenario(result.scenario) + } + is SuccessIterationResult -> append("No error was found.") + else -> throw IllegalStateException("Unsupported IterationResult to be reported.") + } + }.toString() + inline fun log(logLevel: LoggingLevel, crossinline msg: () -> String) { if (this.logLevel > logLevel) return out.println(msg()) @@ -116,7 +146,7 @@ private fun StringBuilder.appendExecutionScenario(scenario: ExecutionScenario) { } } -fun StringBuilder.appendIncorrectResults(scenario: ExecutionScenario, results: ExecutionResult) { +private fun StringBuilder.appendIncorrectResults(scenario: ExecutionScenario, results: ExecutionResult) { appendln("= Invalid execution results: =") if (scenario.initExecution.isNotEmpty()) { appendln("Init part:") @@ -130,4 +160,17 @@ fun StringBuilder.appendIncorrectResults(scenario: ExecutionScenario, results: E appendln("Post part:") append(uniteActorsAndResults(scenario.postExecution, results.postResults)) } +} + +private fun StringBuilder.appendExceptionStackTrace(e: Throwable) { + val sw = StringWriter() + val pw = PrintWriter(sw) + val reducedStackTrace = mutableListOf() + for (ste in e.stackTrace) { + if (ste.className.startsWith("org.jetbrains.kotlinx.lincheck.runner.")) break + reducedStackTrace.add(ste) + } + e.stackTrace = reducedStackTrace.toTypedArray() + e.printStackTrace(pw) + append(sw.toString()) } \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.java deleted file mode 100644 index 0a1ff8718..000000000 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.java +++ /dev/null @@ -1,77 +0,0 @@ -package org.jetbrains.kotlinx.lincheck.execution; - -/* - * #%L - * Lincheck - * %% - * Copyright (C) 2015 - 2018 Devexperts, LLC - * %% - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU Lesser General Public License as - * published by the Free Software Foundation, either version 3 of the - * License, or (at your option) any later version. - * - * This program 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 Lesser Public License for more details. - * - * You should have received a copy of the GNU General Lesser Public - * License along with this program. If not, see - * . - * #L% - */ - -import org.jetbrains.kotlinx.lincheck.Result; - -import java.util.List; -import java.util.Objects; - -/** - * This class represents a result corresponding to - * the specified {@link ExecutionScenario scenario} execution. - *

- * All the result parts should have the same dimensions as the scenario. - */ -public class ExecutionResult { - /** - * Results of the initial sequential part of the execution. - * @see ExecutionScenario#initExecution - */ - public final List initResults; - /** - * Results of the parallel part of the execution. - * @see ExecutionScenario#parallelExecution - */ - public final List> parallelResults; - /** - * Results of the last sequential part of the execution. - * @see ExecutionScenario#postExecution - */ - public final List postResults; - - public ExecutionResult(List initResults, List> parallelResults, List postResults) { - this.initResults = initResults; - this.parallelResults = parallelResults; - this.postResults = postResults; - } - - @Override - public boolean equals(Object o) { - if (this == o) { - return true; - } - if (o == null || getClass() != o.getClass()) { - return false; - } - ExecutionResult that = (ExecutionResult) o; - return Objects.equals(initResults, that.initResults) && - Objects.equals(parallelResults, that.parallelResults) && - Objects.equals(postResults, that.postResults); - } - - @Override - public int hashCode() { - return Objects.hash(initResults, parallelResults, postResults); - } -} diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt new file mode 100644 index 000000000..3a1042634 --- /dev/null +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionResult.kt @@ -0,0 +1,27 @@ +package org.jetbrains.kotlinx.lincheck.execution + +import org.jetbrains.kotlinx.lincheck.* + +/** + * This class represents a result corresponding to + * the specified [scenario][ExecutionScenario] execution. + * + * All the result parts should have the same dimensions as the scenario. + */ +data class ExecutionResult( + /** + * Results of the initial sequential part of the execution. + * @see ExecutionScenario.initExecution + */ + val initResults: List, + /** + * Results of the parallel part of the execution. + * @see ExecutionScenario.parallelExecution + */ + val parallelResults: List>, + /** + * Results of the last sequential part of the execution. + * @see ExecutionScenario.postExecution + */ + val postResults: List +) \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.java index a52874a11..0e21fe7a9 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/execution/ExecutionScenario.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.execution; - /* * #%L * Lincheck @@ -10,17 +8,18 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.execution; import org.jetbrains.kotlinx.lincheck.Actor; import org.jetbrains.kotlinx.lincheck.strategy.Strategy; diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/InvocationResult.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/InvocationResult.kt new file mode 100644 index 000000000..6549a2d52 --- /dev/null +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/InvocationResult.kt @@ -0,0 +1,66 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.runner + +import org.jetbrains.kotlinx.lincheck.execution.* + +/** + * Represents results for invocations, see [Runner.run]. + * Marked as error (see [isError]) if this invocation has been failed. + */ +internal sealed class InvocationResult { + abstract val isError: Boolean +} + +/** + * The invocation completed successfully with correct results. + */ +internal object SuccessfulInvocationResult: InvocationResult() { + override val isError get() = false +} + +/** + * The invocation completed successfully, but the [results] are incorrect. + */ +internal data class IncorrectInvocationResult( + val results: ExecutionResult +) : InvocationResult() { + override val isError get() = true +} + +/** + * Indicates that the invocation has get into deadlock or livelock. + */ +internal data class DeadlockInvocationResult( + val threadDump: Map> +) : InvocationResult() { + override val isError get() = true +} + +/** + * The invocation has finished with an unexpected exception. + */ +internal class UnexpectedExceptionInvocationResult( + val exception: Throwable +) : InvocationResult() { + override val isError get() = true +} \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/IterationResult.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/IterationResult.kt new file mode 100644 index 000000000..de0623388 --- /dev/null +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/IterationResult.kt @@ -0,0 +1,22 @@ +package org.jetbrains.kotlinx.lincheck.runner + +import org.jetbrains.kotlinx.lincheck.execution.* + +sealed class IterationResult { + abstract val isError: Boolean +} + +internal object SuccessfulIterationResult : IterationResult() { + override val isError: Boolean get() = false +} + +internal class IncorrectIterationResult(val scenario: ExecutionResult, val result: ExecutionResult) : IterationResult() { + override val isError: Boolean get() = true +} + +internal class FailedIterationResult(val failedInvocationResult: InvocationResult) : IterationResult() { + init { + require(failedInvocationResult.isError) { "The provided invocation result should be a failure" } + } + override val isError: Boolean get() = true +} \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt index 03629b644..c02ffc163 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/ParallelThreadsRunner.kt @@ -40,7 +40,7 @@ private typealias SuspensionPointResultWithContinuation = AtomicReference, @@ -48,6 +48,7 @@ open class ParallelThreadsRunner( ) : Runner(scenario, strategy, testClass) { private lateinit var testInstance: Any private val executor = newFixedThreadPool(scenario.threads, ParallelThreadsRunner::TestThread) + private val completedOrSuspendedThreads = AtomicInteger(0) private val completions = List(scenario.threads) { threadId -> List(scenario.parallelExecution[threadId].size) { Completion(threadId) } @@ -163,41 +164,34 @@ open class ParallelThreadsRunner( return suspensionPointResults[threadId] } - override fun run(): ExecutionResult? { + override fun run(): InvocationResult { reset() - val initResults = scenario.initExecution.map { initActor -> executeActor(testInstance, initActor) } - val parallelResults = testThreadExecutions.map { executor.submit(it) }.map { future -> - try { - future.get(10, TimeUnit.SECONDS).toList() - } catch (e: TimeoutException) { - val stackTraces = Thread.getAllStackTraces().filter { (t, _) -> t is TestThread } - val msgBuilder = StringBuilder() - msgBuilder.appendln("The execution has hung, see the thread dump:") - for ((t, stackTrace) in stackTraces) { - t as TestThread - msgBuilder.appendln("Thread-${t.iThread}:") - for (ste in stackTrace) { - if (ste.className.startsWith("org.jetbrains.kotlinx.lincheck.runner.")) break - msgBuilder.appendln("\t$ste") - } - msgBuilder.appendln() + try { + val initResults = scenario.initExecution.map { initActor -> executeActor(testInstance, initActor) } + val parallelResults = testThreadExecutions.map { executor.submit(it) }.map { future -> + try { + future.get(10, TimeUnit.SECONDS).toList() + } catch (e: TimeoutException) { + val threadDump = Thread.getAllStackTraces().filter { (t, _) -> t is TestThread } + threadDump.keys.forEach { it.stop() } + return DeadlockInvocationResult(threadDump) } - Thread.getAllStackTraces().map { it.key }.filterIsInstance().forEach { it.stop() } - throw AssertionError(msgBuilder.toString()) } - } - val dummyCompletion = Continuation(EmptyCoroutineContext) {} - var postPartSuspended = false - val postResults = scenario.postExecution.map { postActor -> - // no actors are executed after suspension of a post part - if (postPartSuspended) { - NoResult - } else { - // post part may contain suspendable actors if there aren't any in the parallel part, invoke with dummy continuation - executeActor(testInstance, postActor, dummyCompletion).also { postPartSuspended = it.wasSuspended } + val dummyCompletion = Continuation(EmptyCoroutineContext) {} + var postPartSuspended = false + val postResults = scenario.postExecution.map { postActor -> + // no actors are executed after suspension of a post part + if (postPartSuspended) { + NoResult + } else { + // post part may contain suspendable actors if there aren't any in the parallel part, invoke with dummy continuation + executeActor(testInstance, postActor, dummyCompletion).also { postPartSuspended = it.wasSuspended } + } } + return CompletedInvocationResult(ExecutionResult(initResults, parallelResults, postResults)) + } catch (e: Throwable) { + return UnexpectedExceptionInvocationResult(e) } - return ExecutionResult(initResults, parallelResults, postResults) } override fun onStart(iThread: Int) { diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/Runner.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/Runner.java index b2a8686ea..1e65bc18f 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/Runner.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/runner/Runner.java @@ -1,34 +1,32 @@ -package org.jetbrains.kotlinx.lincheck.runner; - /* * #%L * Lincheck * %% * Copyright (C) 2015 - 2018 Devexperts, LLC + * Copyright (C) 2019 JetBrains s.r.o. * %% * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ -import org.jetbrains.kotlinx.lincheck.ExecutionClassLoader; -import org.jetbrains.kotlinx.lincheck.TransformationClassLoader; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; -import org.jetbrains.kotlinx.lincheck.strategy.Strategy; -import org.objectweb.asm.ClassVisitor; -import java.util.concurrent.atomic.AtomicInteger; +package org.jetbrains.kotlinx.lincheck.runner; + +import org.jetbrains.kotlinx.lincheck.*; +import org.jetbrains.kotlinx.lincheck.execution.*; +import org.jetbrains.kotlinx.lincheck.strategy.*; +import org.objectweb.asm.*; /** * Runner determines how to run your concurrent test. In order to support techniques @@ -40,7 +38,6 @@ public abstract class Runner { protected final ExecutionScenario scenario; protected final Class testClass; public final ExecutionClassLoader classLoader; - protected final AtomicInteger completedOrSuspendedThreads = new AtomicInteger(0); protected Runner(ExecutionScenario scenario, Strategy strategy, Class testClass) { this.scenario = scenario; @@ -79,10 +76,9 @@ public boolean needsTransformation() { } /** - * Runs next invocation - * @return the obtained results + * Runs the next invocation. */ - public abstract ExecutionResult run() throws InterruptedException; + public abstract InvocationResult run() throws InterruptedException; /** * This method is invoked by every test thread as the first operation. @@ -101,11 +97,4 @@ public void onFinish(int iThread) {} * Closes used for this runner resources. */ public void close() {} - - /** - * @return whether all scenario threads are completed or suspended - */ - public boolean isParallelExecutionCompleted() { - return completedOrSuspendedThreads.get() == scenario.getThreads(); - } } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/ManagedStrategy.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/ManagedStrategy.java index bcb771c9c..137c4c52a 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/ManagedStrategy.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/ManagedStrategy.java @@ -23,13 +23,14 @@ */ import org.jetbrains.kotlinx.lincheck.Reporter; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; +import org.jetbrains.kotlinx.lincheck.runner.InvocationResult; import org.jetbrains.kotlinx.lincheck.runner.ParallelThreadsRunner; import org.jetbrains.kotlinx.lincheck.runner.Runner; -import org.jetbrains.kotlinx.lincheck.verifier.Verifier; import org.objectweb.asm.ClassVisitor; +import java.util.*; + /** * This is an abstract class for all managed strategies. * This abstraction helps to choose a proper {@link Runner}, @@ -45,8 +46,8 @@ public abstract class ManagedStrategy extends Strategy { private final Runner runner; private ManagedStrategyTransformer transformer; - protected ManagedStrategy(Class testClass, ExecutionScenario scenario, Verifier verifier, Reporter reporter) { - super(scenario, verifier, reporter); + protected ManagedStrategy(Class testClass, ExecutionScenario scenario, Reporter reporter) { + super(scenario, reporter); nThreads = scenario.parallelExecution.size(); runner = new ParallelThreadsRunner(scenario, this, testClass, null) { @Override @@ -75,9 +76,9 @@ public boolean needsTransformation() { } @Override - public final void run() throws Exception { + public final List run() throws Exception { try { - runImpl(); + return runImpl(); } finally { runner.close(); } @@ -88,7 +89,7 @@ public final void run() throws Exception { * * @return invocation results for each executed actor. */ - protected final ExecutionResult runInvocation() throws InterruptedException { + protected final InvocationResult runInvocation() throws InterruptedException { return runner.run(); } @@ -103,10 +104,8 @@ protected final StackTraceElement getLocationDescription(int codeLocation) { /** * This method implements the strategy logic - * - * @throws Exception an occurred exception (at least by {@link Verifier}) during the testing */ - protected abstract void runImpl() throws Exception; + protected abstract List runImpl() throws Exception; // == LISTENING EVENTS == diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/Strategy.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/Strategy.java index cee57d59e..7a43aec6c 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/Strategy.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/Strategy.java @@ -22,18 +22,14 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.CTestConfiguration; -import org.jetbrains.kotlinx.lincheck.Reporter; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; -import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchCTestConfiguration; -import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.RandomSwitchStrategy; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTestConfiguration; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressStrategy; -import org.jetbrains.kotlinx.lincheck.verifier.Verifier; -import org.objectweb.asm.ClassVisitor; +import org.jetbrains.kotlinx.lincheck.*; +import org.jetbrains.kotlinx.lincheck.execution.*; +import org.jetbrains.kotlinx.lincheck.runner.*; +import org.jetbrains.kotlinx.lincheck.strategy.randomswitch.*; +import org.jetbrains.kotlinx.lincheck.strategy.stress.*; +import org.objectweb.asm.*; -import static org.jetbrains.kotlinx.lincheck.ReporterKt.appendIncorrectResults; +import java.util.*; /** * Implementation of this class describes how to run the generated execution. @@ -45,22 +41,12 @@ public abstract class Strategy { protected final ExecutionScenario scenario; protected final Reporter reporter; - private final Verifier verifier; - protected Strategy(ExecutionScenario scenario, Verifier verifier, Reporter reporter) { + protected Strategy(ExecutionScenario scenario, Reporter reporter) { this.scenario = scenario; - this.verifier = verifier; this.reporter = reporter; } - protected void verifyResults(ExecutionResult results) { - if (!verifier.verifyResults(results)) { - StringBuilder msgBuilder = new StringBuilder("Invalid interleaving found:\n"); - appendIncorrectResults(msgBuilder, scenario, results); - throw new AssertionError(msgBuilder.toString()); - } - } - public ClassVisitor createTransformer(ClassVisitor cv) { throw new UnsupportedOperationException(getClass() + " runner does not transform classes"); } @@ -73,17 +59,16 @@ public boolean needsTransformation() { * Creates {@link Strategy} based on {@code testCfg} type. */ public static Strategy createStrategy(CTestConfiguration testCfg, Class testClass, - ExecutionScenario scenario, Verifier verifier, Reporter reporter) - { + ExecutionScenario scenario, Reporter reporter) { if (testCfg instanceof StressCTestConfiguration) { - return new StressStrategy(testClass, scenario, verifier, + return new StressStrategy(testClass, scenario, (StressCTestConfiguration) testCfg, reporter); } else if (testCfg instanceof RandomSwitchCTestConfiguration) { - return new RandomSwitchStrategy(testClass, scenario, verifier, + return new RandomSwitchStrategy(testClass, scenario, (RandomSwitchCTestConfiguration) testCfg, reporter); } throw new IllegalArgumentException("Unknown strategy configuration type: " + testCfg.getClass()); } - public abstract void run() throws Exception; -} + public abstract List run() throws Exception; +} \ No newline at end of file diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchStrategy.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchStrategy.java index ca2aee2c2..8ddab75b0 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchStrategy.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/randomswitch/RandomSwitchStrategy.java @@ -22,10 +22,12 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.Reporter; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; -import org.jetbrains.kotlinx.lincheck.strategy.ManagedStrategy; -import org.jetbrains.kotlinx.lincheck.verifier.Verifier; +import org.jetbrains.kotlinx.lincheck.*; +import org.jetbrains.kotlinx.lincheck.execution.*; +import org.jetbrains.kotlinx.lincheck.runner.*; +import org.jetbrains.kotlinx.lincheck.strategy.*; + +import java.util.*; /** * This managed strategy switches current thread to a random one with the specified probability. @@ -37,16 +39,19 @@ public class RandomSwitchStrategy extends ManagedStrategy { private final int invocations; public RandomSwitchStrategy(Class testClass, ExecutionScenario scenario, - Verifier verifier, RandomSwitchCTestConfiguration testCfg, Reporter reporter) + RandomSwitchCTestConfiguration testCfg, Reporter reporter) { - super(testClass, scenario, verifier, reporter); + super(testClass, scenario, reporter); this.invocations = testCfg.invocationsPerIteration; } @Override - protected void runImpl() throws Exception { - for (int i = 0; i < invocations; i++) - verifyResults(runInvocation()); + protected List runImpl() throws Exception { + List results = new ArrayList<>(); + for (int i = 1; i < invocations; i++) { + results.add(runInvocation()); + } + return results; } @Override diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.java index 52183b5c9..a83abcb2e 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/strategy/stress/StressStrategy.java @@ -22,19 +22,13 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.Actor; -import org.jetbrains.kotlinx.lincheck.Reporter; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; -import org.jetbrains.kotlinx.lincheck.runner.ParallelThreadsRunner; -import org.jetbrains.kotlinx.lincheck.runner.Runner; -import org.jetbrains.kotlinx.lincheck.strategy.Strategy; -import org.jetbrains.kotlinx.lincheck.verifier.Verifier; +import org.jetbrains.kotlinx.lincheck.*; +import org.jetbrains.kotlinx.lincheck.execution.*; +import org.jetbrains.kotlinx.lincheck.runner.*; +import org.jetbrains.kotlinx.lincheck.strategy.*; -import java.util.ArrayList; -import java.util.List; -import java.util.Random; -import java.util.concurrent.Phaser; -import java.util.concurrent.atomic.AtomicInteger; +import java.util.*; +import java.util.concurrent.atomic.*; /** * This strategy @@ -50,8 +44,8 @@ public class StressStrategy extends Strategy { private final AtomicInteger uninitializedThreads = new AtomicInteger(0); // for threads synchronization public StressStrategy(Class testClass, ExecutionScenario scenario, - Verifier verifier, StressCTestConfiguration testCfg, Reporter reporter) { - super(scenario, verifier, reporter); + StressCTestConfiguration testCfg, Reporter reporter) { + super(scenario, reporter); this.invocations = testCfg.invocationsPerIteration; // Create waits if needed waits = testCfg.addWaits ? new ArrayList<>() : null; @@ -61,7 +55,6 @@ public StressStrategy(Class testClass, ExecutionScenario scenario, } } // Create runner - Phaser phaser = new Phaser(testCfg.threads); runner = new ParallelThreadsRunner(scenario, this, testClass, waits) { @Override public void onStart(int iThread) { @@ -73,10 +66,11 @@ public void onStart(int iThread) { } @Override - public void run() throws InterruptedException { + public List run() throws InterruptedException { try { + List results = new ArrayList<>(); // Run invocations - for (int invocation = 0; invocation < invocations; invocation++) { + for (int invocation = 1; invocation <= invocations; invocation++) { // Specify waits if needed if (waits != null) { int maxWait = (int) ((float) invocation * MAX_WAIT / invocations) + 1; @@ -87,8 +81,11 @@ public void run() throws InterruptedException { } } uninitializedThreads.set(scenario.parallelExecution.size()); // reinit synchronization - verifyResults(runner.run()); + InvocationResult r = runner.run(); + results.add(r); + if (r.isError()) break; } + return results; } finally { runner.close(); } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/AbstractLTSVerifier.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/AbstractLTSVerifier.kt index 9ca4bc42d..98ff146bf 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/AbstractLTSVerifier.kt +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/AbstractLTSVerifier.kt @@ -33,11 +33,11 @@ import org.jetbrains.kotlinx.lincheck.execution.* * the next possible transitions using [VerifierContext.nextContext] function. This verifier * uses depth-first search to find a proper path. */ -abstract class AbstractLTSVerifier(protected val scenario: ExecutionScenario, protected val sequentialSpecification: Class<*>) : CachedVerifier() { +abstract class AbstractLTSVerifier(protected val sequentialSpecification: Class<*>) : CachedVerifier() { abstract val lts: LTS - abstract fun createInitialContext(results: ExecutionResult): VerifierContext + abstract fun createInitialContext(scenario: ExecutionScenario, results: ExecutionResult): VerifierContext - override fun verifyResultsImpl(results: ExecutionResult) = createInitialContext(results).verify() + override fun verifyResultsImpl(scenario: ExecutionScenario, results: ExecutionResult) = createInitialContext(scenario, results).verify() private fun VerifierContext.verify(): Boolean { // Check if a possible path is found. diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java index 990f62a8d..412fe387a 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/CachedVerifier.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.verifier; - /* * #%L * Lincheck @@ -10,22 +8,24 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; +package org.jetbrains.kotlinx.lincheck.verifier; + +import org.jetbrains.kotlinx.lincheck.execution.*; -import java.util.HashSet; -import java.util.Set; +import java.util.*; +import java.util.concurrent.*; /** * This verifier cached the already verified results in a hash table, @@ -34,14 +34,13 @@ * phase significantly. */ public abstract class CachedVerifier implements Verifier { - private final Set previousResults = new HashSet<>(); + private final ConcurrentHashMap> previousResults = new ConcurrentHashMap<>(); @Override - public final boolean verifyResults(ExecutionResult results) { - if (!previousResults.add(results)) - return true; - return verifyResultsImpl(results); + public final boolean verifyResults(ExecutionScenario scenario, ExecutionResult results) { + Map previousScenarioResults = previousResults.computeIfAbsent(scenario, s -> new HashMap<>()); + return previousScenarioResults.computeIfAbsent(results, r -> verifyResultsImpl(scenario, r)); } - public abstract boolean verifyResultsImpl(ExecutionResult results); + public abstract boolean verifyResultsImpl(ExecutionScenario scenario, ExecutionResult results); } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/EpsilonVerifier.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/EpsilonVerifier.java index 578b56d6c..234da2f33 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/EpsilonVerifier.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/EpsilonVerifier.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.verifier; - /* * #%L * Lincheck @@ -10,30 +8,30 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.verifier; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; +import org.jetbrains.kotlinx.lincheck.execution.*; /** * This verifier does nothing and could be used for performance benchmarking. */ public class EpsilonVerifier implements Verifier { - public EpsilonVerifier(ExecutionScenario scenario, Class sequentialSpecification) {} + public EpsilonVerifier(Class sequentialSpecification) {} @Override - public boolean verifyResults(ExecutionResult results) { + public boolean verifyResults(ExecutionScenario scenario, ExecutionResult results) { return true; // Always correct results :) } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt index 4ce604c79..9478ec400 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/LTS.kt @@ -82,6 +82,7 @@ class LTS(sequentialSpecification: Class<*>) { /** * Computes or gets the existing transition from the current state by the given [actor]. */ + @Synchronized fun next(actor: Actor, expectedResult: Result, ticket: Int) = if (ticket == NO_TICKET) nextByRequest(actor, expectedResult) else nextByFollowUp(actor, ticket, expectedResult) @@ -111,6 +112,7 @@ class LTS(sequentialSpecification: Class<*>) { return if (transitionInfo.isLegalByFollowUp(expectedResult)) transitionInfo else null } + @Synchronized fun nextByCancellation(actor: Actor, ticket: Int): TransitionInfo = transitionsByCancellations.computeIfAbsent(ticket) { generateNextState { instance, suspendedOperations, resumedTicketsWithResults, continuationsMap -> // Invoke the given operation to count the next transition. @@ -231,7 +233,8 @@ class LTS(sequentialSpecification: Class<*>) { /** * Creates and stores the new LTS state or gets the one if already exists. */ - private inline fun StateInfo.intern( + @Synchronized + private fun StateInfo.intern( curOperation: Operation?, block: (StateInfo, RemappingFunction?) -> T ): T { diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/SerializabilityVerifier.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/SerializabilityVerifier.java index 8692dda21..1ae772750 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/SerializabilityVerifier.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/SerializabilityVerifier.java @@ -22,7 +22,6 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier; @@ -38,8 +37,8 @@ public class SerializabilityVerifier extends CachedVerifier { private final LinearizabilityVerifier linearizabilityVerifier; - public SerializabilityVerifier(ExecutionScenario scenario, Class sequentialSpecification) { - this.linearizabilityVerifier = new LinearizabilityVerifier(convertScenario(scenario), sequentialSpecification); + public SerializabilityVerifier(Class sequentialSpecification) { + this.linearizabilityVerifier = new LinearizabilityVerifier(sequentialSpecification); } private static List> convert(List initPart, List> parallelPart, List postPart) { @@ -66,8 +65,8 @@ private static ExecutionResult convertResult(ExecutionResult scenario) { } @Override - public boolean verifyResultsImpl(ExecutionResult results) { - return linearizabilityVerifier.verifyResultsImpl(convertResult(results)); + public boolean verifyResultsImpl(ExecutionScenario scenario, ExecutionResult results) { + return linearizabilityVerifier.verifyResultsImpl(convertScenario(scenario), convertResult(results)); } @Override diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/Verifier.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/Verifier.java index 13b9e7470..03146030d 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/Verifier.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/Verifier.java @@ -22,7 +22,7 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; +import org.jetbrains.kotlinx.lincheck.execution.*; import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier; /** @@ -30,7 +30,7 @@ * By default, it checks for linearizability (see {@link LinearizabilityVerifier}). *

* IMPORTANT! - * All implementations should have {@code (ExecutionScenario scenario, Class sequentialSpecification)} constructor, + * All implementations should have {@code (Class sequentialSpecification)} constructor, * which takes the scenario to be tested and the correct sequential implementation of the testing data structure. */ public interface Verifier { @@ -38,7 +38,7 @@ public interface Verifier { * Verifies the specified results for correctness. * Returns {@code true} if results are possible, {@code false} otherwise. */ - boolean verifyResults(ExecutionResult results); + boolean verifyResults(ExecutionScenario scenario, ExecutionResult results); /** * Verifiers which use sequential implementation instances as states (or parts of them) diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt index 9d4dc7f63..a5746e752 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt @@ -35,12 +35,11 @@ import org.jetbrains.kotlinx.lincheck.verifier.* * for performance improvement (see [CachedVerifier]). */ class LinearizabilityVerifier( - scenario: ExecutionScenario, sequentialSpecification: Class<*> -) : AbstractLTSVerifier(scenario, sequentialSpecification) { +) : AbstractLTSVerifier(sequentialSpecification) { override val lts: LTS = LTS(sequentialSpecification = sequentialSpecification) - override fun createInitialContext(results: ExecutionResult) = + override fun createInitialContext(scenario: ExecutionScenario, results: ExecutionResult) = LinearizabilityContext(scenario, results, lts.initialState) } diff --git a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quiescent/QuiescentConsistencyVerifier.java b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quiescent/QuiescentConsistencyVerifier.java index 20b1b1083..951365c77 100644 --- a/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quiescent/QuiescentConsistencyVerifier.java +++ b/lincheck/src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quiescent/QuiescentConsistencyVerifier.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.verifier.quiescent; - /* * #%L * Lincheck @@ -10,35 +8,31 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.verifier.quiescent; -import org.jetbrains.kotlinx.lincheck.Actor; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionScenario; -import org.jetbrains.kotlinx.lincheck.verifier.CachedVerifier; -import org.jetbrains.kotlinx.lincheck.verifier.linearizability.LinearizabilityVerifier; +import org.jetbrains.kotlinx.lincheck.*; +import org.jetbrains.kotlinx.lincheck.execution.*; +import org.jetbrains.kotlinx.lincheck.verifier.*; +import org.jetbrains.kotlinx.lincheck.verifier.linearizability.*; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; +import java.util.*; public class QuiescentConsistencyVerifier extends CachedVerifier { - private final ExecutionScenario originalScenario; private final LinearizabilityVerifier linearizabilityVerifier; - public QuiescentConsistencyVerifier(ExecutionScenario scenario, Class sequentialSpecification) { - this.originalScenario = scenario; - this.linearizabilityVerifier = new LinearizabilityVerifier(convertScenario(scenario), sequentialSpecification); + public QuiescentConsistencyVerifier(Class sequentialSpecification) { + this.linearizabilityVerifier = new LinearizabilityVerifier(sequentialSpecification); } private static ExecutionScenario convertScenario(ExecutionScenario scenario) { @@ -69,11 +63,13 @@ private static boolean isQuiescentConsistent(Actor actor) { } @Override - public boolean verifyResultsImpl(ExecutionResult results) { - return linearizabilityVerifier.verifyResultsImpl(new ExecutionResult( - results.initResults, - convertAccordingToScenario(originalScenario.parallelExecution, results.parallelResults), - results.postResults) + public boolean verifyResultsImpl(ExecutionScenario scenario, ExecutionResult results) { + return linearizabilityVerifier.verifyResultsImpl(convertScenario(scenario), + new ExecutionResult( + results.initResults, + convertAccordingToScenario(scenario.parallelExecution, results.parallelResults), + results.postResults + ) ); } diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/AbstractLinCheckTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/AbstractLinCheckTest.kt new file mode 100644 index 000000000..c2ebd3ddc --- /dev/null +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/AbstractLinCheckTest.kt @@ -0,0 +1,54 @@ +/*- + * #%L + * Lincheck + * %% + * Copyright (C) 2019 JetBrains s.r.o. + * %% + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as + * published by the Free Software Foundation, either version 3 of the + * License, or (at your option) any later version. + * + * This program 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 Lesser Public License for more details. + * + * You should have received a copy of the GNU General Lesser Public + * License along with this program. If not, see + * . + * #L% + */ +package org.jetbrains.kotlinx.lincheck.test + +import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult +import org.jetbrains.kotlinx.lincheck.strategy.SuccessIterationResult +import org.jetbrains.kotlinx.lincheck.strategy.stress.StressOptions +import org.jetbrains.kotlinx.lincheck.verifier.VerifierState +import org.junit.Assert.assertTrue +import org.junit.Test +import kotlin.reflect.KClass +import kotlin.reflect.full.isSubclassOf + +/** + * An abstraction for testing all lincheck strategies + */ +abstract class AbstractLinCheckTest(vararg expectedErrors: KClass) : VerifierState() { + private val expectedErrors = if (expectedErrors.isEmpty()) listOf(SuccessIterationResult::class) else expectedErrors.toList() + private val reporter = Reporter(LoggingLevel.INFO) + + override fun extractState() = error("Not implemented") + + open fun > O.customizeOptions(): O = this + + private fun runTest(createOptions: () -> Options<*, *>) { + val result = LinChecker.checkDetailed(this.javaClass, createOptions()).values.first().last() + assertTrue(reporter.generateReport(result), expectedErrors.any { expectedError -> result::class.isSubclassOf(expectedError)}) + } + + @Test(timeout = 100_000) + fun testWithStressStrategy() = runTest { + StressOptions().iterations(30).customizeOptions() + } +} diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ExceptionAsResultTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ExceptionAsResultTest.java index 1d85ba724..78f4adcd5 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ExceptionAsResultTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ExceptionAsResultTest.java @@ -22,7 +22,6 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; import org.junit.Test; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/HangingTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/HangingTest.kt index c29126ec6..12f78673d 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/HangingTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/HangingTest.kt @@ -23,17 +23,17 @@ package org.jetbrains.kotlinx.lincheck.test import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* -import org.jetbrains.kotlinx.lincheck.strategy.stress.* -import org.junit.* +import org.jetbrains.kotlinx.lincheck.strategy.* -@StressCTest(iterations = 1, actorsBefore = 0, actorsAfter = 0, - requireStateEquivalenceImplCheck = false, minimizeFailedScenario = false) -class HangingTest { +class HangingTest : AbstractLinCheckTest(DeadlockIterationResult::class) { @Operation fun badOperation() { while (true) {} } - @Test(expected = AssertionError::class) - fun test() = LinChecker.check(this::class.java) + override fun extractState() = Unit + + override fun > O.customizeOptions(): O = + iterations(1).actorsBefore(0).actorsAfter(0) + .requireStateEquivalenceImplCheck(false).minimizeFailedScenario(false) } diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/NonParallelOpGroupTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/NonParallelOpGroupTest.java index 73e2a0000..478b5a734 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/NonParallelOpGroupTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/NonParallelOpGroupTest.java @@ -22,28 +22,25 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; -import org.jetbrains.kotlinx.lincheck.LoggingLevel; -import org.jetbrains.kotlinx.lincheck.annotations.LogLevel; -import org.jetbrains.kotlinx.lincheck.annotations.OpGroupConfig; +import org.jctools.queues.atomic.*; +import org.jetbrains.annotations.*; +import org.jetbrains.kotlinx.lincheck.*; import org.jetbrains.kotlinx.lincheck.annotations.Operation; -import org.jetbrains.kotlinx.lincheck.annotations.Param; -import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; -import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; -import org.jctools.queues.atomic.SpscLinkedAtomicQueue; -import org.junit.Test; +import org.jetbrains.kotlinx.lincheck.annotations.*; +import org.jetbrains.kotlinx.lincheck.strategy.stress.*; +import org.jetbrains.kotlinx.lincheck.verifier.*; +import org.junit.*; -import java.util.concurrent.atomic.AtomicInteger; +import java.util.*; @OpGroupConfig(name = "producer", nonParallel = true) @OpGroupConfig(name = "consumer", nonParallel = true) -@StressCTest(requireStateEquivalenceImplCheck = false) -public class NonParallelOpGroupTest { +@StressCTest(iterations = 50, actorsPerThread = 3) +public class NonParallelOpGroupTest extends VerifierState { private SpscLinkedAtomicQueue queue = new SpscLinkedAtomicQueue<>(); - private AtomicInteger i = new AtomicInteger(); @Operation(group = "producer") - public void offer(@Param(gen = IntGen.class) Integer x) { + public void offer(Integer x) { queue.offer(x); } @@ -52,9 +49,16 @@ public Integer poll() { return queue.poll(); } - @Operation - public int incAndGet() { - return i.incrementAndGet(); + @NotNull + @Override + protected Object extractState() { + List elements = new ArrayList<>(); + while (true) { + Integer el = poll(); + if (el == null) break; + elements.add(el); + } + return elements; } @Test diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ResultAsParameterTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ResultAsParameterTest.java index e93294f24..1862fe3d1 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ResultAsParameterTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/ResultAsParameterTest.java @@ -22,7 +22,6 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.OpGroupConfig; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.annotations.Param; @@ -35,7 +34,7 @@ import java.util.List; @OpGroupConfig(name = "push_remove", nonParallel = true) -@StressCTest +@StressCTest(iterations = 10, actorsBefore = 0, actorsPerThread = 2, actorsAfter = 0) public class ResultAsParameterTest extends VerifierState { private Stack stack = new Stack(); private Node lastPushNode = null; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/RunOnceTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/RunOnceTest.java index 67f1addf8..b49e8fe8a 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/RunOnceTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/RunOnceTest.java @@ -22,14 +22,13 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; import org.junit.Test; -@StressCTest(threads = 3, iterations = 100, invocationsPerIteration = 10, requireStateEquivalenceImplCheck = false) +@StressCTest(threads = 3, iterations = 10, invocationsPerIteration = 10, requireStateEquivalenceImplCheck = false) public class RunOnceTest { - private A a = new A();; + private A a = new A(); @Operation(runOnce = true) public void a() { diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/ParallelThreadsRunnerEasyExceptionTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/ParallelThreadsRunnerEasyExceptionTest.kt index bd3bacd5b..40cb46720 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/ParallelThreadsRunnerEasyExceptionTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/ParallelThreadsRunnerEasyExceptionTest.kt @@ -25,6 +25,8 @@ import org.jetbrains.kotlinx.lincheck.runner.ParallelThreadsRunner import org.junit.Test import kotlin.coroutines.intrinsics.* import org.jetbrains.kotlinx.lincheck.* +import org.jetbrains.kotlinx.lincheck.runner.CompletedInvocationResult +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult import org.jetbrains.kotlinx.lincheck.strategy.Strategy import org.jetbrains.kotlinx.lincheck.test.verifier.* import org.junit.Assert.assertEquals @@ -86,7 +88,7 @@ class SuspendResumeScenarios { class ParallelThreadsRunnerExceptionTest { val mockStrategy = object : Strategy(null, null, null) { - override fun run() { + override fun run(): IterationResult { throw UnsupportedOperationException() } } @@ -114,10 +116,9 @@ class ParallelThreadsRunnerExceptionTest { } } } - val runner = - ParallelThreadsRunner(scenario, mockStrategy, testClass, null) - val results = runner.run() - assertEquals(results, expectedResults) + val runner = ParallelThreadsRunner(scenario, mockStrategy, testClass, null) + val invocationResult = runner.run() + assertEquals((invocationResult as CompletedInvocationResult).results, expectedResults) } @Test @@ -135,8 +136,8 @@ class ParallelThreadsRunnerExceptionTest { } } val runner = ParallelThreadsRunner(scenario, mockStrategy, testClass, null) - val results = runner.run() - assertEquals(results, expectedResults) + val invocationResult = runner.run() + assertEquals((invocationResult as CompletedInvocationResult).results, expectedResults) } @Test @@ -148,10 +149,9 @@ class ParallelThreadsRunnerExceptionTest { } } } - val runner = - ParallelThreadsRunner(scenario, mockStrategy, testClass, null) - val results = runner.run() - assertEquals(results, expectedResults) + val runner = ParallelThreadsRunner(scenario, mockStrategy, testClass, null) + val invocationResult = runner.run() + assertEquals((invocationResult as CompletedInvocationResult).results, expectedResults) } } diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/TestThreadExecutionHelperTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/TestThreadExecutionHelperTest.java index c59e72176..f844b0287 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/TestThreadExecutionHelperTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/runner/TestThreadExecutionHelperTest.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.test.runner; - /* * #%L * Lincheck @@ -10,23 +8,25 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.test.runner; import org.jetbrains.kotlinx.lincheck.*; -import org.jetbrains.kotlinx.lincheck.execution.ExecutionResult; +import org.jetbrains.kotlinx.lincheck.runner.InvocationResult; import org.jetbrains.kotlinx.lincheck.runner.Runner; import org.jetbrains.kotlinx.lincheck.runner.TestThreadExecution; import org.jetbrains.kotlinx.lincheck.runner.TestThreadExecutionGenerator; +import org.jetbrains.kotlinx.lincheck.strategy.IterationResult; import org.jetbrains.kotlinx.lincheck.strategy.Strategy; import org.junit.Assert; import org.junit.Before; @@ -45,13 +45,13 @@ public class TestThreadExecutionHelperTest { public void setUp() { Strategy mockStrategy = new Strategy(null, null, null) { @Override - public void run(){ + public IterationResult run(){ throw new UnsupportedOperationException(); } }; runner = new Runner(null, mockStrategy, ArrayDeque.class) { @Override - public ExecutionResult run() { + public InvocationResult run() { throw new UnsupportedOperationException(); } }; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchCTestAnnTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchCTestAnnTest.java index 72fb8a5a5..9259f53db 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchCTestAnnTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchCTestAnnTest.java @@ -22,7 +22,6 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator; import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchOptionsTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchOptionsTest.java index 980d87f71..380ef3793 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchOptionsTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/randomswitch/RandomSwitchOptionsTest.java @@ -22,7 +22,6 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.Options; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressCTestAnnTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressCTestAnnTest.java index 80f545b17..c0da59290 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressCTestAnnTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressCTestAnnTest.java @@ -22,8 +22,6 @@ * #L% */ -import org.jetbrains.annotations.NotNull; -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.execution.RandomExecutionGenerator; import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressOptionsTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressOptionsTest.java index edbb6bccb..c362a388b 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressOptionsTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/strategy/stress/StressOptionsTest.java @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.test.strategy.stress; - /* * #%L * Lincheck @@ -10,19 +8,19 @@ * it under the terms of the GNU Lesser General Public License as * published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. - * + * * This program 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 Lesser Public License for more details. - * + * * You should have received a copy of the GNU General Lesser Public * License along with this program. If not, see * . * #L% */ +package org.jetbrains.kotlinx.lincheck.test.strategy.stress; -import org.jetbrains.kotlinx.lincheck.LinChecker; import org.jetbrains.kotlinx.lincheck.LoggingLevel; import org.jetbrains.kotlinx.lincheck.Options; import org.jetbrains.kotlinx.lincheck.annotations.Operation; @@ -51,7 +49,7 @@ public void test() { .verifier(LinearizabilityVerifier.class) .threads(2) .actorsPerThread(3) - .logLevel(LoggingLevel.INFO) + .logLevel(LoggingLevel.ERROR) .requireStateEquivalenceImplCheck(false) .minimizeFailedScenario(false); LinChecker.check(StressOptionsTest.class, opts); diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt index 187ffd98f..433316cd2 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/CustomScenarioDSL.kt @@ -60,7 +60,7 @@ fun verify( val (scenario, results) = scenarioWithResults(block) val verifier = verifierClass.getConstructor(ExecutionScenario::class.java, Class::class.java) .newInstance(scenario, testClass) - val res = verifier.verifyResults(results) + val res = verifier.verifyResults(scenario, results) assert(res == correct) } diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/EpsilonVerifierTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/EpsilonVerifierTest.kt index 19593cf59..3fa08d373 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/EpsilonVerifierTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/EpsilonVerifierTest.kt @@ -1,5 +1,3 @@ -package org.jetbrains.kotlinx.lincheck.test.verifier - /* * #%L * Lincheck @@ -21,6 +19,7 @@ package org.jetbrains.kotlinx.lincheck.test.verifier * . * #L% */ +package org.jetbrains.kotlinx.lincheck.test.verifier import org.jetbrains.kotlinx.lincheck.LinChecker import org.jetbrains.kotlinx.lincheck.annotations.Operation @@ -29,7 +28,7 @@ import org.jetbrains.kotlinx.lincheck.verifier.EpsilonVerifier import org.jetbrains.kotlinx.lincheck.verifier.VerifierState import org.junit.Test -@StressCTest(verifier = EpsilonVerifier::class) +@StressCTest(iterations = 10, threads = 2, actorsPerThread = 2, verifier = EpsilonVerifier::class) class EpsilonVerifierTest : VerifierState() { private var i = 0 diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/BufferedChannelStressTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/BufferedChannelStressTest.kt index 552cce0aa..caf6af3a6 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/BufferedChannelStressTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/BufferedChannelStressTest.kt @@ -21,16 +21,18 @@ */ package org.jetbrains.kotlinx.lincheck.test.verifier.linearizability +import kotlinx.coroutines.* import kotlinx.coroutines.channels.* import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.paramgen.* import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.test.* import org.junit.* +@InternalCoroutinesApi @Param(name = "value", gen = IntGen::class, conf = "1:5") -@StressCTest(actorsPerThread = 3, sequentialSpecification = SequentiaBuffered2IntChannel::class) -class BufferedChannelStressTest { +class BufferedChannelStressTest : AbstractLinCheckTest() { private val c = Channel(2) @Operation(cancellableOnSuspension = false) @@ -45,8 +47,9 @@ class BufferedChannelStressTest { @Operation fun offer(@Param(name = "value") value: Int) = c.offer(value) - @Test - fun test() = LinChecker.check(BufferedChannelStressTest::class.java) + override fun > O.customizeOptions(): O = + sequentialSpecification(SequentiaBuffered2IntChannel::class.java) } +@InternalCoroutinesApi class SequentiaBuffered2IntChannel : SequentialIntChannel(capacity = 2) \ No newline at end of file diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/RendezvousChannelStressTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/RendezvousChannelStressTest.kt index 76ab40111..50b96aaa1 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/RendezvousChannelStressTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/RendezvousChannelStressTest.kt @@ -21,34 +21,36 @@ */ package org.jetbrains.kotlinx.lincheck.test.verifier.linearizability +import kotlinx.coroutines.* import kotlinx.coroutines.channels.* import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* import org.jetbrains.kotlinx.lincheck.paramgen.* import org.jetbrains.kotlinx.lincheck.strategy.stress.* +import org.jetbrains.kotlinx.lincheck.test.* import org.jetbrains.kotlinx.lincheck.verifier.linearizability.* import org.junit.* -@LogLevel(LoggingLevel.DEBUG) +@InternalCoroutinesApi @Param(name = "value", gen = IntGen::class, conf = "1:5") -@StressCTest(sequentialSpecification = SequentialRendezvousIntChannel::class, verifier = LinearizabilityVerifier::class) -class RendezvousChannelStressTest { +class RendezvousChannelStressTest : AbstractLinCheckTest() { private val ch = Channel() @Operation(handleExceptionsAsResult = [ClosedSendChannelException::class]) suspend fun send(@Param(name = "value") value: Int) = ch.send(value) @Operation(handleExceptionsAsResult = [ClosedReceiveChannelException::class]) - suspend fun receive() = ch.receive() + 100 + suspend fun receive() = ch.receive() @Operation(handleExceptionsAsResult = [ClosedReceiveChannelException::class]) - suspend fun receiveOrNull() = ch.receiveOrNull()?.plus(100) + suspend fun receiveOrNull() = ch.receiveOrNull() @Operation fun close() = ch.close() - @Test - fun test() = LinChecker.check(RendezvousChannelStressTest::class.java) + override fun > O.customizeOptions(): O = + sequentialSpecification(SequentialRendezvousIntChannel::class.java) } +@InternalCoroutinesApi class SequentialRendezvousIntChannel : SequentialIntChannel(capacity = 0) \ No newline at end of file diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/SequentialIntChannel.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/SequentialIntChannel.kt index 994121762..fe8fdbbf3 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/SequentialIntChannel.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/linearizability/SequentialIntChannel.kt @@ -24,102 +24,74 @@ package org.jetbrains.kotlinx.lincheck.test.verifier.linearizability import kotlinx.coroutines.* import kotlinx.coroutines.channels.* import org.jetbrains.kotlinx.lincheck.verifier.* -import java.util.concurrent.locks.* -import kotlin.coroutines.* +@InternalCoroutinesApi open class SequentialIntChannel(private val capacity: Int) : VerifierState() { - private val lock = ReentrantLock() private val senders = ArrayList, Int>>() - private val receivers = ArrayList>() - private val buffer = ArrayList(capacity) + private val receivers = ArrayList>() + private val buffer = ArrayList() private var closed = false - @InternalCoroutinesApi suspend fun send(x: Int) { - lock.lock() - try { - if (offer(x)) return - suspendAtomicCancellableCoroutine { cont -> - senders.add(cont to x) - } - } finally { - lock.unlock() + if (offer(x)) return + suspendAtomicCancellableCoroutine { cont -> + senders.add(cont to x) } } - @InternalCoroutinesApi fun offer(x: Int): Boolean { - lock.lock() - try { - while (true) { - if (closed) throw ClosedSendChannelException("") - if (receivers.isEmpty() && buffer.size == capacity) return false - if (receivers.isNotEmpty()) { - val r = receivers.removeAt(0) - if (r.tryResume0(x)) return true - } else { - buffer.add(x) - return true - } + while (true) { + if (closed) throw ClosedSendChannelException("") + if (receivers.isNotEmpty()) { + val r = receivers.removeAt(0) + if (r.tryResume0(x)) return true + } else { + if (buffer.size == capacity) return false + buffer.add(x) + return true } - } finally { - lock.unlock() } } - @InternalCoroutinesApi suspend fun receive(): Int { - lock.lock() - try { - val pollResult = poll() - if (pollResult !== null) return pollResult - return suspendAtomicCancellableCoroutine { cont -> - receivers.add(cont) - } - } finally { - lock.unlock() - } + val res = receiveImpl() + if (res === CLOSED) throw ClosedReceiveChannelException("") + return res as Int } @InternalCoroutinesApi suspend fun receiveOrNull(): Int? { - lock.lock() - try { - if (senders.isEmpty() && closed) return null - val pollResult = poll() - if (pollResult !== null) return pollResult - return suspendAtomicCancellableCoroutine { cont -> - receivers.add(cont) - } - } finally { - lock.unlock() + val res = receiveImpl() + return if (res === CLOSED) null + else res as Int + } + + suspend fun receiveImpl(): Any { + if (buffer.isEmpty() && senders.isEmpty() && closed) return CLOSED + val pollResult = poll() + if (pollResult !== null) return pollResult + return suspendAtomicCancellableCoroutine { cont -> + receivers.add(cont) } } - @InternalCoroutinesApi fun poll(): Int? { - lock.lock() - try { - if (buffer.size > 0) { - val res = buffer.removeAt(0) - while (true) { - if (senders.isEmpty()) break - val (s, x) = senders.removeAt(0) - if (s.tryResume0(Unit)) { - buffer.add(x) - break - } - } - return res - } + if (buffer.size > 0) { + val res = buffer.removeAt(0) while (true) { - if (senders.isEmpty() && closed) throw ClosedReceiveChannelException("") - if (senders.isEmpty()) return null + if (senders.isEmpty()) break val (s, x) = senders.removeAt(0) - if (s.tryResume0(Unit)) return x + if (s.tryResume0(Unit)) { + buffer.add(x) + break + } } - } finally { - lock.unlock() + return res + } + while (true) { + if (senders.isEmpty()) return null + val (s, x) = senders.removeAt(0) + if (s.tryResume0(Unit)) return x } } @@ -127,7 +99,7 @@ open class SequentialIntChannel(private val capacity: Int) : VerifierState() { if (closed) return false closed = true receivers.forEach { - it.resumeWithException(ClosedReceiveChannelException("")) + it.tryResume0(CLOSED) } receivers.clear() return true @@ -142,3 +114,5 @@ private fun CancellableContinuation.tryResume0(res: T): Boolean { completeResume(token) return true } + +private val CLOSED = Any() \ No newline at end of file diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/quiescent/LockFreeMPSCQueueTest.java b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/quiescent/LockFreeMPSCQueueTest.java index a69833d81..0e6fad09c 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/quiescent/LockFreeMPSCQueueTest.java +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/quiescent/LockFreeMPSCQueueTest.java @@ -22,20 +22,25 @@ * #L% */ -import org.jetbrains.kotlinx.lincheck.LinChecker; +import kotlin.*; +import org.jetbrains.annotations.*; import org.jetbrains.kotlinx.lincheck.annotations.OpGroupConfig; import org.jetbrains.kotlinx.lincheck.annotations.Operation; import org.jetbrains.kotlinx.lincheck.annotations.Param; import org.jetbrains.kotlinx.lincheck.paramgen.IntGen; import org.jetbrains.kotlinx.lincheck.strategy.stress.StressCTest; +import org.jetbrains.kotlinx.lincheck.verifier.*; import org.jetbrains.kotlinx.lincheck.verifier.quiescent.QuiescentConsistencyVerifier; import org.jetbrains.kotlinx.lincheck.verifier.quiescent.QuiescentConsistent; import org.junit.Test; -@StressCTest(verifier = QuiescentConsistencyVerifier.class, requireStateEquivalenceImplCheck = false) +import java.util.*; + +@StressCTest(iterations = 50, actorsBefore = 0, actorsPerThread = 2, verifier = QuiescentConsistencyVerifier.class) @OpGroupConfig(name = "consumer", nonParallel = true) -public class LockFreeMPSCQueueTest { +public class LockFreeMPSCQueueTest extends VerifierState { private LockFreeMPSCQueue q = new LockFreeMPSCQueue<>(); + private boolean closed = false; @Operation(group = "consumer") @QuiescentConsistent @@ -52,6 +57,19 @@ public boolean addLast(@Param(gen = IntGen.class) Integer val) { @QuiescentConsistent public void close() { q.close(); + closed = true; + } + + @NotNull + @Override + protected Object extractState() { + List elements = new ArrayList<>(); + while (true) { + Integer el = removeFirstOrNull(); + if (el == null) break; + elements.add(el); + } + return new Pair<>(elements, closed); } @Test diff --git a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/serializability/SerializableQueueSimulationTest.kt b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/serializability/SerializableQueueSimulationTest.kt index 3cb38f093..54787d259 100644 --- a/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/serializability/SerializableQueueSimulationTest.kt +++ b/lincheck/src/test/java/org/jetbrains/kotlinx/lincheck/test/verifier/serializability/SerializableQueueSimulationTest.kt @@ -24,18 +24,17 @@ package org.jetbrains.kotlinx.lincheck.test.verifier.serializability import org.jetbrains.kotlinx.lincheck.* import org.jetbrains.kotlinx.lincheck.annotations.* +import org.jetbrains.kotlinx.lincheck.annotations.Operation import org.jetbrains.kotlinx.lincheck.paramgen.* import org.jetbrains.kotlinx.lincheck.strategy.stress.* -import org.jetbrains.kotlinx.lincheck.verifier.SerializabilityVerifier +import org.jetbrains.kotlinx.lincheck.verifier.* import org.junit.Test -@StressCTest(actorsBefore = 2, - threads = 2, actorsPerThread = 4, - actorsAfter = 2, - verifier = SerializabilityVerifier::class) -class SerializableQueueSimulationTest { - val q = SerializableQueueSimulation() +@StressCTest(iterations = 30, actorsBefore = 1, threads = 2, actorsPerThread = 2, actorsAfter = 2, + verifier = SerializabilityVerifier::class, requireStateEquivalenceImplCheck = false) +class SerializableQueueSimulationTest : VerifierState() { + private val q = SerializableQueueSimulation() @Operation fun push(@Param(gen = IntGen::class) item: Int) = q.push(item) @@ -45,19 +44,4 @@ class SerializableQueueSimulationTest { @Test fun test() = LinChecker.check(SerializableQueueSimulationTest::class.java) - - override fun equals(other: Any?): Boolean { - if (this === other) return true - if (javaClass != other?.javaClass) return false - - other as SerializableQueueSimulationTest - - if (q != other.q) return false - - return true - } - - override fun hashCode(): Int { - return q.hashCode() - } }