Skip to content

Commit

Permalink
Done
Browse files Browse the repository at this point in the history
  • Loading branch information
ndkoval committed Mar 28, 2024
1 parent 6b3dab7 commit b5dc8c9
Show file tree
Hide file tree
Showing 44 changed files with 1,070 additions and 1,272 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 Down Expand Up @@ -44,6 +44,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 b5dc8c9

Please sign in to comment.