-
Notifications
You must be signed in to change notification settings - Fork 34
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Review + make the structure more consistent (in progress) + parallel …
…verification (in progress)
- Loading branch information
Showing
104 changed files
with
1,769 additions
and
2,813 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
171 changes: 171 additions & 0 deletions
171
libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Accounts.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
* <http://www.gnu.org/licenses/lgpl-3.0.html>. | ||
* #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<Integer, Integer> 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); | ||
} | ||
} |
66 changes: 66 additions & 0 deletions
66
libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/Counters.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
* <http://www.gnu.org/licenses/lgpl-3.0.html>. | ||
* #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() | ||
} |
104 changes: 104 additions & 0 deletions
104
libtest/src/main/java/org/jetbrains/kotlinx/lincheck/tests/custom/LockBasedSets.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
* <http://www.gnu.org/licenses/lgpl-3.0.html>. | ||
* #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<Int>() | ||
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<Int>() | ||
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<Int>() | ||
|
||
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<Int>() | ||
|
||
@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) | ||
} |
Oops, something went wrong.