Relaxed contracts restored

README.md

@@ -1,4 +1,4 @@
-# kotlinx-lincheck
+1# kotlinx-lincheck
 
 [![JetBrains incubator project](https://jb.gg/badges/incubator.svg)](https://confluence.jetbrains.com/display/ALL/JetBrains+on+GitHub)
 [![License: LGPL v3](https://img.shields.io/badge/License-LGPL%20v3-blue.svg)](https://www.gnu.org/licenses/lgpl-3.0)

src/main/java/org/jetbrains/kotlinx/lincheck/Utils.kt

@@ -66,19 +66,28 @@ fun createCostCounterInstance(costCounter: Class<*>, relaxationFactor: Int): Any
     }
 }
 
-internal fun executeActor(testInstance: Any, actor: Actor) = executeActor(testInstance, actor, null)
+internal fun executeActor(testInstance: Any, actor: Actor) = executeActor(testInstance, actor, null, null)
+internal fun executeActor(testInstance: Any, actor: Actor, completion: Continuation<Any?>?) =
+        executeActor(testInstance, actor, completion, null)
 
 /**
  * Executes the specified actor on the sequential specification instance and returns its result.
  */
 internal fun executeActor(
     instance: Any,
     actor: Actor,
-    completion: Continuation<Any?>?
+    completion: Continuation<Any?>?,
+    result: Result?
 ): Result {
     try {
-        val m = getMethod(instance, actor.method)
-        val args = if (actor.isSuspendable) actor.arguments + completion else actor.arguments
+        val m = if (result == null) getMethod(instance, actor.method)
+        else getRelaxedMethod(instance, actor.method)
+        val args = when {
+            actor.isSuspendable && result != null -> actor.arguments + result + completion
+            actor.isSuspendable -> actor.arguments + completion
+            result != null -> actor.arguments + result
+            else -> actor.arguments
+        }
         val res = m.invoke(instance, *args.toTypedArray())
         return if (m.returnType.isAssignableFrom(Void.TYPE)) VoidResult else createLincheckResult(res)
     } catch (invE: Throwable) {
@@ -132,6 +141,15 @@ private fun getMethod(instance: Any, method: Method): Method {
     }
 }
 
+private fun getRelaxedMethod(instance: Any, method: Method): Method {
+    val methods = methodsCache.computeIfAbsent(instance.javaClass) { WeakHashMap() }
+    return methods[method]?.get() ?: run {
+        val m = instance.javaClass.getMethod(method.name, *(method.parameterTypes + Result::class.java))
+        methods[method] = WeakReference(m)
+        m
+    }
+}
+
 /**
  * Creates [Result] of corresponding type from any given value.
  *

src/main/java/org/jetbrains/kotlinx/lincheck/verifier/AbstractLTSVerifier.kt

@@ -45,8 +45,9 @@ abstract class AbstractLTSVerifier(protected val sequentialSpecification: Class<
         // Traverse through next possible transitions using depth-first search (DFS). Note that
         // initial and post parts are represented as threads with ids `0` and `threads + 1` respectively.
         for (threadId in threads) {
-            val nextContext = nextContext(threadId)
-            if (nextContext !== null && nextContext.verify()) return true
+            for (nextContext in nextContexts(threadId)) {
+                if (nextContext.verify()) return true
+            }
         }
         return false
     }
@@ -92,7 +93,7 @@ abstract class VerifierContext(
     /**
      * Counts next possible states and the corresponding contexts if the specified thread is executed.
      */
-    abstract fun nextContext(threadId: Int): VerifierContext?
+    abstract fun nextContexts(threadId: Int): List<VerifierContext>
 
     /**
      * Returns `true` if all actors in the specified thread are executed.

src/main/java/org/jetbrains/kotlinx/lincheck/verifier/linearizability/LinearizabilityVerifier.kt

@@ -47,8 +47,8 @@ class LinearizabilityContext : VerifierContext {
     constructor(scenario: ExecutionScenario, results: ExecutionResult, state: LTS.State,
                 executed: IntArray, suspended: BooleanArray, tickets: IntArray) : super(scenario, results, state, executed, suspended, tickets)
 
-    override fun nextContext(threadId: Int): LinearizabilityContext? {
-        if (isCompleted(threadId)) return null
+    override fun nextContexts(threadId: Int): List<LinearizabilityContext> {
+        if (isCompleted(threadId)) return emptyList()
         // Check whether an actorWithToken from the specified thread can be executed
         // in accordance with the rule that all actors from init part should be
         // executed at first, after that all actors from parallel part, and
@@ -58,19 +58,22 @@ class LinearizabilityContext : VerifierContext {
             in 1..scenario.threads -> isCompleted(0) && hblegal(threadId) // PARALLEL
             else -> initCompleted && parallelCompleted // POST
         }
-        if (!legal) return null
+        if (!legal) return emptyList()
         val actorId = executed[threadId]
         val actor = scenario[threadId][actorId]
         val expectedResult = results[threadId][actorId]
         // Check whether the operation has been suspended and should be followed by cancellation
         if (suspended[threadId]) {
-            return if (actor.cancelOnSuspension && expectedResult === Cancelled)
-                state.nextByCancellation(actor, tickets[threadId]).createContext(threadId)
-            else null
+            return if (actor.cancelOnSuspension && expectedResult === Cancelled) {
+                val nextContext = state.nextByCancellation(actor, tickets[threadId], expectedResult)?.createContext(threadId)
+                if (nextContext != null) listOf(nextContext) else emptyList()
+            }
+            else emptyList()
         }
         // Try to make transition by the next actor from the current thread,
         // passing the ticket corresponding to the current thread.
-        return state.next(actor, expectedResult, tickets[threadId])?.createContext(threadId)
+        val nextContext = state.next(actor, expectedResult, tickets[threadId])?.createContext(threadId)
+        return if (nextContext != null) listOf(nextContext) else emptyList()
     }
 
     // checks whether the transition does not violate the happens-before relation constructed on the clocks

src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quantitative/CostWithNextCostCounter.java

@@ -0,0 +1,77 @@
+package org.jetbrains.kotlinx.lincheck.verifier.quantitative;
+
+/*
+ * #%L
+ * Lincheck
+ * %%
+ * 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%
+ */
+
+
+/**
+ * This class is used to define possible transitions in {@link QuantitativelyRelaxedLinearizabilityVerifier}.
+ *
+ * @param <COST_COUNTER> cost counter class for the testing data structure.
+ *                       It have to be defined for cleaner code.
+ */
+public class CostWithNextCostCounter<COST_COUNTER> {
+    /**
+     * Instance of the next cost counter instance.
+     */
+    public COST_COUNTER nextCostCounter;
+
+    /**
+     * The transition cost.
+     */
+    public int cost;
+
+    /**
+     * It is {@code true} if the transition predicate is satisfied.
+     * By default {@code cost != 0} predicate is used.
+     */
+    public boolean predicate;
+
+    /**
+     * Create new cost counter transition with the specified state and cost.
+     * This constructor defines {@link #predicate transition predicate} at {@code cost != 0}.
+     */
+    public CostWithNextCostCounter(COST_COUNTER nextCostCounter, int cost) {
+        this.nextCostCounter = nextCostCounter;
+        this.cost = cost;
+        this.predicate = cost != 0;
+    }
+
+    /**
+     * Create new cost counter transition with the specified state and cost.
+     * This constructor defines {@link #predicate transition predicate} at {@code cost != 0}.
+     */
+    public CostWithNextCostCounter(COST_COUNTER nextCostCounter, boolean predicate) {
+        this.nextCostCounter = nextCostCounter;
+        this.cost = Integer.MAX_VALUE;
+        this.predicate = predicate;
+    }
+
+    /**
+     * Create new cost counter transition with the specified state, cost and predicate satisfaction.
+     */
+    public CostWithNextCostCounter(COST_COUNTER nextCostCounter, int cost, boolean predicate) {
+        this.nextCostCounter = nextCostCounter;
+        this.cost = cost;
+        this.predicate = predicate;
+    }
+}

src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quantitative/IterativePathCostFunctionCounter.kt

@@ -0,0 +1,36 @@
+package org.jetbrains.kotlinx.lincheck.verifier.quantitative
+
+/*
+ * #%L
+ * Lincheck
+ * %%
+ * 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%
+ */
+
+/**
+ * Implementation of this interface counts path cost incrementally.
+ */
+interface IterativePathCostFunctionCounter {
+    /**
+     * Returns next path cost counter with the required information for incremental counting
+     * if the transition is possible, {@code null} if the transition is not satisfied.
+     *
+     * @param costWithNextCostCounter describes the transition
+     */
+    fun next(cost: Int, predicate: Boolean = (cost != 0)): IterativePathCostFunctionCounter?
+}

src/main/java/org/jetbrains/kotlinx/lincheck/verifier/quantitative/PathCostFunction.java

@@ -0,0 +1,165 @@
+package org.jetbrains.kotlinx.lincheck.verifier.quantitative;
+
+/*
+ * #%L
+ * Lincheck
+ * %%
+ * 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%
+ */
+
+/**
+ * Defines strategy to count a path cost according to the
+ * "Quantitative relaxation of concurrent data structures"
+ * paper by Henzinger, T. A., Kirsch, C. M., Payer, H.,
+ * Sezgin, A., & Sokolova, A. (paragraph 4.3)
+ */
+public enum PathCostFunction {
+    /**
+     * Non-relaxed cost strategy checks that the transition cost equals zero.
+     */
+    NON_RELAXED {
+        IterativePathCostFunctionCounter nonRelaxedPathCostFunctionCounter = null;
+
+        @Override
+        public IterativePathCostFunctionCounter createIterativePathCostFunctionCounter(int relaxationFactor) {
+            return NON_RELAXED_PATH_COST_FUNCTION_COUNTER_SINGLETON;
+        }
+    },
+    /**
+     * Maximal cost strategy checks that the maximal transition cost
+     * is less than the relaxation factor, ignores predicates.
+     * <p>
+     * More formally, <tt>pcost = max{cost_i | 1 <= i <= n}</tt>,
+     * where <tt>cost_i</tt> is the cost of the <tt>i</tt>-th transition.
+     */
+    MAX {
+        @Override
+        public IterativePathCostFunctionCounter createIterativePathCostFunctionCounter(int relaxationFactor) {
+            return new MaxIterativePathCostFunctionCounter(relaxationFactor);
+        }
+    },
+    /**
+     * Phi-interval strategy checks that the maximal subtrace length where the predicate is satisfied
+     * is less than the relaxation factor, ignores costs.
+     * <p>
+     * More formally, <tt>pcost = max{j - i + 1 | phi(i, j) and 1 <= i <= j <= n}</tt>,
+     * where <tt>phi(i, j)</tt> means that predicate is satisfied on <tt>[i, j]</tt> subtrace.
+     */
+    PHI_INTERVAL {
+        @Override
+        public IterativePathCostFunctionCounter createIterativePathCostFunctionCounter(int relaxationFactor) {
+            return new PhiIntervalPathCostFunction(relaxationFactor);
+        }
+    },
+    /**
+     * Phi-interval restricted maximal cost strategy combines both {@link #MAX maximal}
+     * and {@link #PHI_INTERVAL phi-interval} ones.
+     * <p>
+     * <tt>pcost = max{l(i, j) | phi(i, j) and 1 <= i <= j <= n}</tt>,
+     * where <tt>l(i, j) = max{cost_r + (r - i + 1) | i <= r <= j}</tt>.
+     */
+    PHI_INTERVAL_RESTRICTED_MAX {
+        @Override
+        public IterativePathCostFunctionCounter createIterativePathCostFunctionCounter(int relaxationFactor) {
+            return new PhiIntervalRestrictedMaxPathCostFunction(relaxationFactor);
+        }
+    };
+
+    public abstract IterativePathCostFunctionCounter createIterativePathCostFunctionCounter(int relaxationFactor);
+
+    private static class NonRelaxedPathCostFunctionCounter implements IterativePathCostFunctionCounter {
+        @Override
+        public IterativePathCostFunctionCounter next(int cost, boolean predicate) {
+            if (cost != 0) throw new IllegalArgumentException("All costs should be zero");
+            return this;
+        }
+    }
+    private static final NonRelaxedPathCostFunctionCounter NON_RELAXED_PATH_COST_FUNCTION_COUNTER_SINGLETON = new NonRelaxedPathCostFunctionCounter();
+
+    private static class MaxIterativePathCostFunctionCounter implements IterativePathCostFunctionCounter {
+        private final int relaxationFactor;
+
+        MaxIterativePathCostFunctionCounter(int relaxationFactor) {
+            this.relaxationFactor = relaxationFactor;
+        }
+
+        @Override
+        public IterativePathCostFunctionCounter next(int cost, boolean predicate) {
+            return cost < relaxationFactor ? this : null;
+        }
+    }
+
+    private static class PhiIntervalPathCostFunction implements IterativePathCostFunctionCounter {
+        private final int relaxationFactor;
+        private final int predicateSatisfactionCount;
+        private final PhiIntervalPathCostFunction[] cache;
+
+        PhiIntervalPathCostFunction(int relaxationFactor) {
+            this(relaxationFactor, 0, new PhiIntervalPathCostFunction[relaxationFactor]);
+            this.cache[0] = this;
+        }
+
+        private PhiIntervalPathCostFunction(int relaxationFactor, int predicateSatisfactionCount, PhiIntervalPathCostFunction[] cache) {
+            this.relaxationFactor = relaxationFactor;
+            this.predicateSatisfactionCount = predicateSatisfactionCount;
+            this.cache = cache;
+        }
+
+        @Override
+        public IterativePathCostFunctionCounter next(int cost, boolean predicate) {
+            int newPredicateSatisfactionCount = predicate ? predicateSatisfactionCount + 1 : 0;
+            // Check that the transition is possible
+            if (newPredicateSatisfactionCount >= relaxationFactor)
+                return null;
+            // Get cached function counter
+            IterativePathCostFunctionCounter res = cache[newPredicateSatisfactionCount];
+            if (res == null)
+                res = cache[newPredicateSatisfactionCount] = new PhiIntervalPathCostFunction(relaxationFactor, newPredicateSatisfactionCount, cache);
+            return res;
+        }
+    }
+
+    private static class PhiIntervalRestrictedMaxPathCostFunction implements IterativePathCostFunctionCounter {
+        final int relaxationFactor;
+        final int predicateSatisfactionCount;
+        private final PhiIntervalRestrictedMaxPathCostFunction[] cache;
+
+        PhiIntervalRestrictedMaxPathCostFunction(int relaxationFactor) {
+            this(relaxationFactor, 0, new PhiIntervalRestrictedMaxPathCostFunction[relaxationFactor]);
+        }
+
+        private PhiIntervalRestrictedMaxPathCostFunction(int relaxationFactor, int predicateSatisfactionCount, PhiIntervalRestrictedMaxPathCostFunction[] cache) {
+            this.relaxationFactor = relaxationFactor;
+            this.predicateSatisfactionCount = predicateSatisfactionCount;
+            this.cache = cache;
+        }
+
+        @Override
+        public PhiIntervalRestrictedMaxPathCostFunction next(int cost, boolean predicate) {
+            // Check that the transition is possible
+            if (predicateSatisfactionCount + cost >= relaxationFactor)
+                return null;
+            int newPredicateSatisfactionCount = predicate ? predicateSatisfactionCount + 1 : 0;
+            // Get cached function counter
+            PhiIntervalRestrictedMaxPathCostFunction res = cache[newPredicateSatisfactionCount];
+            if (res == null)
+                res = cache[newPredicateSatisfactionCount] = new PhiIntervalRestrictedMaxPathCostFunction(relaxationFactor, newPredicateSatisfactionCount, cache);
+            return res;
+        }
+    }
+}