Skip to content

Commit

Permalink
Done
Browse files Browse the repository at this point in the history
  • Loading branch information
ndkoval committed Apr 5, 2024
1 parent c2617aa commit cdac29d
Show file tree
Hide file tree
Showing 47 changed files with 1,473 additions and 1,306 deletions.
26 changes: 0 additions & 26 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,32 +38,6 @@ dependencies {
}
```

### Java 9+
To use model checking strategy for Java 9 and later, add the following JVM properties:

```text
--add-opens", "java.base/java.lang=ALL-UNNAMED
--add-opens java.base/jdk.internal.misc=ALL-UNNAMED
--add-exports java.base/jdk.internal.util=ALL-UNNAMED
--add-exports java.base/sun.security.action=ALL-UNNAMED
```

They are required if the testing code uses classes from the `java.util` package since
some of them use `jdk.internal.misc.Unsafe` or similar internal classes under the hood.

If you use Gradle, add the following lines to `build.gradle.kts`:

```
tasks.withType<Test> {
jvmArgs(
"--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED",
"--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED",
"--add-exports", "java.base/sun.security.action=ALL-UNNAMED"
)
}
```


## Example

The following Lincheck test easily finds a bug in the standard Java's `ConcurrentLinkedDeque`:
Expand Down
27 changes: 27 additions & 0 deletions bootstrap/build.gradle.kts
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
import org.jetbrains.kotlin.gradle.tasks.*

plugins {
java
kotlin("jvm")
}

repositories {
mavenCentral()
}

sourceSets.main {
java.srcDirs("src")
}

tasks.withType<KotlinCompile> {
kotlinOptions.jvmTarget = "11"
}

tasks.jar {
archiveFileName.set("bootstrap.jar")
}

java {
sourceCompatibility = JavaVersion.VERSION_11
targetCompatibility = JavaVersion.VERSION_11
}
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,15 @@
* with this file, You can obtain one at http://mozilla.org/MPL/2.0/.
*/

package org.jetbrains.kotlinx.lincheck
package sun.nio.ch.lincheck

import java.util.*

/**
* Methods of this interface are called from the instrumented tested code during model-checking.
* See [Injections] for the documentation.
*/
internal interface EventTracker {
interface EventTracker {
fun lock(monitor: Any, codeLocation: Int)
fun unlock(monitor: Any, codeLocation: Int)

Expand All @@ -28,6 +28,7 @@ internal interface EventTracker {

fun beforeReadField(obj: Any, className: String, fieldName: String, codeLocation: Int)
fun beforeReadFieldStatic(className: String, fieldName: String, codeLocation: Int)
fun beforeReadFinalFieldStatic(className: String)
fun beforeReadArrayElement(array: Any, index: Int, codeLocation: Int)
fun afterRead(value: Any?)

Expand All @@ -44,6 +45,9 @@ internal interface EventTracker {
fun getThreadLocalRandom(): Random
fun randomNextInt(): Int

fun onNewObjectCreation(obj: Any)
fun onWriteToObjectFieldOrArrayCell(obj: Any, fieldOrArrayCellValue: Any?)
fun beforeNewObjectCreation(className: String)
fun afterNewObjectCreation(obj: Any)

fun onWriteToObjectFieldOrArrayCell(receiver: Any, fieldOrArrayCellValue: Any?)
fun onWriteObjectToStaticField(fieldValue: Any?)
}
Loading

0 comments on commit cdac29d

Please sign in to comment.