New model checker algorithm #410

eupp · 2024-10-02T12:29:25Z

No description provided.

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* fix monitor tests * fix parking tests (use Unsafe for reflective memory locations read/writes) * fix few bugs by adding `runInIgnoredSection` Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* fix `patchResultsClock` function * remove redundant `AtomicLongTest` * fix delta in managed strategy handler of `getAndIncrement()` and similar methods * remove obsolete code from EventStructureMemoryTracker * perform physical write to memory on successful CAS Signed-off-by: Evgeniy Moiseenko <[email protected]>

* track constructor calls to track allocations of objects whose base classes are not instrumented Signed-off-by: Evgeniy Moiseenko <[email protected]>

* move `loopDetector.initialize()` into `ManagedStrategy.initializeInvocation` * comment debug byte-code printing Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* fix `getFieldAccessMemoryLocation` (use actual runtime object's class name instead of compile-time access class name) * minor clean-up in MemoryTracker.kt Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

…entstruct-mc branch Signed-off-by: Evgeniy Moiseenko <[email protected]>

…ent type is unknown Signed-off-by: Evgeniy Moiseenko <[email protected]>

… new invocation and on new actor start) Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* fix type computation for VarHandle accesses Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* testing new model checking strategy * ensure that the object read from an intercepted read is transformed * repair primitives tests * repair `VarHandleLocalObjectsTest` Signed-off-by: Evgeniy Moiseenko <[email protected]>

* fix expected outcomes for `testLincheckPromptCancellation` Signed-off-by: Evgeniy Moiseenko <[email protected]>

… initialization) Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

… revisit this!) * decrease the number of loop iterations inside test's `operation()`, because currently large number of iterations triggers false-positive live-lock failure, due to naive implementation of spin-loops detection Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

* So, apparently, the `context` used in the `ParallelThreadsRunner::Completion` can somehow escape between different invocations of the test. If this happens, everything becomes really FUCKED UP, and I spent hours trying to debug it. It leads to a situation, when on the new run of the test, an old `ParallelThreadRunnerInterceptor` object (stored in the `context`) from the previous invocation is used instead. To fix the issue, I changed the `Completion::reset` logic. Instead of creating new interceptor object, I re-use the same object by reset its state. Since we only use completions in a very specific way in `ParallelThreadsRunner` (basically one separate completion object for each suspending actor) this should not, in theory, lead to any problem. Still, only Gods know if this is truly correct way to fix this. Signed-off-by: Evgeniy Moiseenko <[email protected]>

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp · 2024-10-02T12:35:34Z

bootstrap/src/sun/nio/ch/lincheck/Injections.java

@@ -250,13 +254,27 @@ public static void afterReflectiveSetter(Object receiver, Object value) {
        getEventTracker().afterReflectiveSetter(receiver, value);
    }

+    public static void onArrayCopy(Object srcArray, int srcPos, Object dstArray, int dstPos, int length) {
+        getEventTracker().onArrayCopy(srcArray, srcPos, dstArray, dstPos, length);
+    }


Add comment about System.arraycopy

eupp · 2024-10-02T12:39:27Z

bootstrap/src/sun/nio/ch/lincheck/Injections.java

                                          boolean isStatic, boolean isFinal) {
        if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadField(obj, className, fieldName, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeReadField(obj, className, fieldName, typeDescriptor, codeLocation, isStatic, isFinal);


Re-check if typeDescriptor is required (find its usages).

Check if isPrimitive: Boolean would be enough.

TODO: Extract into separate PR.

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp · 2025-01-14T10:35:16Z

bootstrap/src/sun/nio/ch/lincheck/Injections.java

                                          boolean isStatic, boolean isFinal) {
        if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadField(obj, className, fieldName, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeReadField(obj, className, fieldName, typeDescriptor, codeLocation, isStatic, isFinal);


Check if isPrimitive: Boolean would be enough.

eupp · 2025-01-14T10:35:51Z

bootstrap/src/sun/nio/ch/lincheck/Injections.java

                                          boolean isStatic, boolean isFinal) {
        if (!isStatic && obj == null) return false; // Ignore, NullPointerException will be thrown
-        return getEventTracker().beforeReadField(obj, className, fieldName, codeLocation, isStatic, isFinal);
+        return getEventTracker().beforeReadField(obj, className, fieldName, typeDescriptor, codeLocation, isStatic, isFinal);


TODO: Extract into separate PR.

eupp · 2025-01-14T10:38:51Z

build.gradle.kts

+            // flags to import Unsafe module;
+            // it is used in some tests to check handling of unsafe APIs by Lincheck
+            "--add-opens", "java.base/jdk.internal.misc=ALL-UNNAMED",
+            "--add-exports", "java.base/jdk.internal.util=ALL-UNNAMED",


Extract Unsafe tests into separate sub-project ?

eupp added 30 commits October 1, 2024 19:23

moved all event-structure-related files from the eventstruct-mc branch

5da52ff

Signed-off-by: Evgeniy Moiseenko <[email protected]>

WIP: fixes after eventstruct-mc branch transferring

3b99739

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes

d5876d9

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes and refactoring

2d6a0c1

* fix monitor tests * fix parking tests (use Unsafe for reflective memory locations read/writes) * fix few bugs by adding `runInIgnoredSection` Signed-off-by: Evgeniy Moiseenko <[email protected]>

transfer atomics tests from eventstruct-mc branch

4b56f1d

Signed-off-by: Evgeniy Moiseenko <[email protected]>

add EXPERIMENTAL_MODEL_CHECKING instrumentation mode

2f16111

Signed-off-by: Evgeniy Moiseenko <[email protected]>

repair object allocation tracking code

bdc40bd

* track constructor calls to track allocations of objects whose base classes are not instrumented Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes

dcabb69

* move `loopDetector.initialize()` into `ManagedStrategy.initializeInvocation` * comment debug byte-code printing Signed-off-by: Evgeniy Moiseenko <[email protected]>

repair EventStructureStrategy spin-loop bounding

1408231

Signed-off-by: Evgeniy Moiseenko <[email protected]>

add array accesses tests

76f58b3

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix in MemoryLocation and MemoryTracker

2ca6978

* fix `getFieldAccessMemoryLocation` (use actual runtime object's class name instead of compile-time access class name) * minor clean-up in MemoryTracker.kt Signed-off-by: Evgeniy Moiseenko <[email protected]>

transfer System.arraycopy instrumentation from eventstruct-mc branch

47c83b2

Signed-off-by: Evgeniy Moiseenko <[email protected]>

ransfer java.lang.reflect.Array.newInstance instrumentation from ev…

7f9acfe

…entstruct-mc branch Signed-off-by: Evgeniy Moiseenko <[email protected]>

add runtime check to avoid intercepting array reads if the array elem…

00f3e3f

…ent type is unknown Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix spin-loop bounding in event-structure strategy (reset counters on…

3df0107

… new invocation and on new actor start) Signed-off-by: Evgeniy Moiseenko <[email protected]>

add VarHandle tests

f819285

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix VarHandle handling logic

40b9d65

* fix type computation for VarHandle accesses Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix onArrayCopy (wrap in ignored section)

4d14db9

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes

38303d1

* testing new model checking strategy * ensure that the object read from an intercepted read is transformed * repair primitives tests * repair `VarHandleLocalObjectsTest` Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes

265ec40

* fix expected outcomes for `testLincheckPromptCancellation` Signed-off-by: Evgeniy Moiseenko <[email protected]>

bugfixing FieldInheritedFromInterfaceTest (problems with static class…

7885bcf

… initialization) Signed-off-by: Evgeniy Moiseenko <[email protected]>

WIP: compilation errors fixes after rebase

8271ed6

Signed-off-by: Evgeniy Moiseenko <[email protected]>

WIP: compilation errors fixes after rebase (in tests)

bd91f74

Signed-off-by: Evgeniy Moiseenko <[email protected]>

restore atomic methods result interception

2194f78

Signed-off-by: Evgeniy Moiseenko <[email protected]>

restore atomic methods result interception

e62b3d3

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix debug stats printing

efaf031

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fixes after rebase (fix invocation initialization logic)

05a0232

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor fixes

8ec1ab7

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix skipping verification of SpinLoopBoundInvocationResult

347a27b

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp added 17 commits October 1, 2024 19:23

minor fixes in trackAtomicMethodMemoryAccess method after rebase

eab0e76

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix bug with clocks (perform deep copy of HBClock objects)

35c6322

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix bug in MethodCallTransformer and repair old model checking strategy

f60ee52

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix event structure execution reset logic for trace collection replay

4cd12c7

Signed-off-by: Evgeniy Moiseenko <[email protected]>

repair ByteArrayAccessTest/BooleanArrayAccessTest

384498a

Signed-off-by: Evgeniy Moiseenko <[email protected]>

better fix for validation actor bug in EventStructureStrategy

81e5655

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix bug in Execution::isEmpty

8fd399c

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor infra fixes

c3a4b13

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix trace collection for the new-mc (do not re-create runner)

cc55529

Signed-off-by: Evgeniy Moiseenko <[email protected]>

bugfix coroutines scheduling and blocking

37a9304

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix duplicate coroutine resume events

3b92001

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fix ParallelThreadsRunner::Completion::context (make it immutable)

43c7db4

Signed-off-by: Evgeniy Moiseenko <[email protected]>

introduce system property to opt-in into experimental model checking

e17af1e

Signed-off-by: Evgeniy Moiseenko <[email protected]>

minor

06de6a6

Signed-off-by: Evgeniy Moiseenko <[email protected]>

fixes after rebase

6b30fbd

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp commented Oct 2, 2024

View reviewed changes

remove obsolete files

c6b9e25

Signed-off-by: Evgeniy Moiseenko <[email protected]>

eupp mentioned this pull request Oct 3, 2024

New model checker #257

Open

15 tasks

eupp commented Jan 14, 2025

View reviewed changes

This was referenced Jan 16, 2025

Add new tests for atomic primitives and array accesses #442

Merged

Modify bytecode injection logic for the new model checking algorithm #443

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New model checker algorithm #410

New model checker algorithm #410

eupp commented Oct 2, 2024

eupp Oct 2, 2024

eupp Oct 2, 2024

eupp Jan 14, 2025

eupp Jan 14, 2025

eupp Jan 14, 2025

eupp Jan 14, 2025

eupp Jan 14, 2025

New model checker algorithm #410

Are you sure you want to change the base?

New model checker algorithm #410

Conversation

eupp commented Oct 2, 2024

eupp Oct 2, 2024

Choose a reason for hiding this comment

eupp Oct 2, 2024

Choose a reason for hiding this comment

eupp Jan 14, 2025

Choose a reason for hiding this comment

eupp Jan 14, 2025

Choose a reason for hiding this comment

eupp Jan 14, 2025

Choose a reason for hiding this comment

eupp Jan 14, 2025

Choose a reason for hiding this comment

eupp Jan 14, 2025

Choose a reason for hiding this comment