Skip to content

Commit

Permalink
Merge pull request #23 from JetBrains-Research/dev-litmus-tests
Browse files Browse the repository at this point in the history
Add more UPUB array tests
  • Loading branch information
DLochmelis33 authored Sep 4, 2024
2 parents 566ea7a + af2284a commit a1935a1
Show file tree
Hide file tree
Showing 3 changed files with 83 additions and 3 deletions.
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package org.jetbrains.litmuskt.tests

import org.jetbrains.litmuskt.autooutcomes.LitmusIOutcome
import org.jetbrains.litmuskt.LitmusTestContainer
import org.jetbrains.litmuskt.autooutcomes.LitmusIOutcome
import org.jetbrains.litmuskt.autooutcomes.accept
import org.jetbrains.litmuskt.autooutcomes.forbid
import org.jetbrains.litmuskt.autooutcomes.interesting
Expand Down Expand Up @@ -72,13 +72,35 @@ object UnsafePublication {
}
}) {
thread {
arr = Array(10) { 0 }
arr = Array(1) { 1 }
}
thread {
r1 = arr?.get(0) ?: -1
}
spec {
accept(0)
accept(1)
// 0 is the default value for `Int`. However, since Int-s in `Array<Int>` are boxed, we don't get to see a 0.
// On JVM, a NullPointerException here is technically valid. Currently, there is no support for exceptions as accepted outcomes.
// On Native, there is no NullPointerException, so we can see a segmentation fault.
interesting(0)
accept(-1)
}
}

val PlainIntArray = litmusTest({
object : LitmusIOutcome() {
var arr: IntArray? = null
}
}) {
thread {
arr = IntArray(1) { 1 }
}
thread {
r1 = arr?.get(0) ?: -1
}
spec {
accept(1)
interesting(0)
accept(-1)
}
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
package org.jetbrains.litmuskt

import org.jetbrains.litmuskt.autooutcomes.LitmusIOutcome
import org.jetbrains.litmuskt.autooutcomes.accept
import org.jetbrains.litmuskt.autooutcomes.forbid
import java.util.concurrent.atomic.AtomicIntegerArray

@LitmusTestContainer
object UnsafePublicationJvm {
val PlainAtomicIntegerArray = litmusTest({
object : LitmusIOutcome() {
var arr: AtomicIntegerArray? = null
}
}) {
thread {
arr = AtomicIntegerArray(intArrayOf(1))
}
thread {
r1 = arr?.get(0) ?: -1
}
spec {
accept(1)
forbid(0)
accept(-1)
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
package org.jetbrains.litmuskt.tests

import org.jetbrains.litmuskt.LitmusTestContainer
import org.jetbrains.litmuskt.autooutcomes.LitmusIOutcome
import org.jetbrains.litmuskt.autooutcomes.accept
import org.jetbrains.litmuskt.autooutcomes.interesting
import org.jetbrains.litmuskt.litmusTest
import kotlin.concurrent.AtomicIntArray

@LitmusTestContainer
object UnsafePublicationNative {

@OptIn(ExperimentalStdlibApi::class)
val PlainAtomicIntArray = litmusTest({
object : LitmusIOutcome() {
var arr: AtomicIntArray? = null
}
}) {
thread {
arr = AtomicIntArray(1) { 1 }
}
thread {
r1 = arr?.get(0) ?: -1
}
spec {
accept(1)
interesting(0)
accept(-1)
}
}
}

0 comments on commit a1935a1

Please sign in to comment.