diff --git a/.github/workflows/run-litmus.yml b/.github/workflows/run-litmus.yml new file mode 100644 index 0000000..63483bd --- /dev/null +++ b/.github/workflows/run-litmus.yml @@ -0,0 +1,50 @@ +name: Run litmus tests on different platforms + +on: + push: + branches: + - dev-gh-ci + - development + - main + +# Note: this CI run is an "integration"-test or "smoke"-test. It is intended to verify that +# the basics of the tool work. It is NOT intended to be complete or to discover weak behaviors. + +jobs: + linux-run: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-java@v4 + with: + distribution: oracle + java-version: 17 + - run: chmod +x gradlew + - name: Assemble CLI binary + run: ./gradlew cli:linkReleaseExecutableLinuxX64 + - name: Run litmus tests via CLI + run: ./cli/build/bin/linuxX64/releaseExecutable/cli.kexe -r pthread ".*" + - name: Run litmus tests with JCStress + # takes ~10 mins + run: ./gradlew :cli:jvmRun --args="-r jcstress -j '-m sanity' .*" + + macos-run: + runs-on: macos-latest + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-java@v4 + with: + distribution: oracle + java-version: 17 + - run: chmod +x gradlew + - name: Assemble CLI binary (x64 + release) + run: ./gradlew cli:linkReleaseExecutableMacosX64 + - name: Run litmus tests via CLI (x64 + release) + run: ./cli/build/bin/macosX64/releaseExecutable/cli.kexe -r pthread ".*" + - name: Run litmus tests with JCStress + # takes ~10 mins + run: ./gradlew :cli:jvmRun --args="-r jcstress -j '-m sanity' .*" + - name: Assemble CLI binary (arm + release) + run: ./gradlew cli:linkReleaseExecutableMacosArm64 + - name: Run litmus tests via CLI (arm + release) + run: ./cli/build/bin/macosArm64/releaseExecutable/cli.kexe -r pthread ".*" diff --git a/cli/src/jvmMain/kotlin/org/jetbrains/litmuskt/CliJvm.kt b/cli/src/jvmMain/kotlin/org/jetbrains/litmuskt/CliJvm.kt index fd4efce..1c16614 100644 --- a/cli/src/jvmMain/kotlin/org/jetbrains/litmuskt/CliJvm.kt +++ b/cli/src/jvmMain/kotlin/org/jetbrains/litmuskt/CliJvm.kt @@ -79,8 +79,17 @@ class CliJvm : CliCommon() { ) JCStressRunner.DEFAULT_LITMUSKT_PARAMS else params // jcstress defaults are different val jcsRunner = runner as JCStressRunner // use the correct runTests()! - val results = jcsRunner.runTests(tests, jcsParams).first() - echo("\n" + results.generateTable()) + val results = jcsRunner.runTests(tests, jcsParams) + + echo() + if (results.isEmpty()) { + echo("no tests were run, perhaps they are missing jcstress wrappers?", err = true) + return + } + results.forEach { (test, result) -> + echo("results for ${test.alias}:") + echo(result.generateTable() + "\n") + } } } } diff --git a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/BooleanAutoOutcomes.kt b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/BooleanAutoOutcomes.kt index 4f1f83f..3ba985c 100644 --- a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/BooleanAutoOutcomes.kt +++ b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/BooleanAutoOutcomes.kt @@ -2,7 +2,11 @@ package org.jetbrains.litmuskt.autooutcomes import org.jetbrains.litmuskt.LitmusOutcomeSpecScope -// TODO +/** + * "Z" is the name for Boolean outcomes in JCStress. + */ + +// TODO: codegen open class LitmusZZOutcome( var r1: Boolean = false, @@ -16,6 +20,10 @@ open class LitmusZZOutcome( } final override fun toList() = listOf(r1, r2) + final override fun parseOutcome(str: String): LitmusZZOutcome { + val rs = str.split(", ").map(String::toBooleanStrict) + return LitmusZZOutcome(rs[0], rs[1]) + } } fun LitmusOutcomeSpecScope.accept(r1: Boolean, r2: Boolean) = diff --git a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/IntAutoOutcomes.kt b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/IntAutoOutcomes.kt index 9ecd149..2eda0e8 100644 --- a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/IntAutoOutcomes.kt +++ b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/IntAutoOutcomes.kt @@ -13,6 +13,10 @@ open class LitmusIOutcome( } final override fun toList() = listOf(r1) + final override fun parseOutcome(str: String): LitmusIOutcome { + val rs = str.split(", ").map(String::toInt) + return LitmusIOutcome(rs[0]) + } } fun LitmusOutcomeSpecScope.accept(r1: Int) = @@ -36,6 +40,10 @@ open class LitmusIIOutcome( } final override fun toList() = listOf(r1, r2) + final override fun parseOutcome(str: String): LitmusIIOutcome { + val rs = str.split(", ").map(String::toInt) + return LitmusIIOutcome(rs[0], rs[1]) + } } fun LitmusOutcomeSpecScope.accept(r1: Int, r2: Int) = @@ -60,6 +68,10 @@ open class LitmusIIIOutcome( } final override fun toList() = listOf(r1, r2, r3) + final override fun parseOutcome(str: String): LitmusIIIOutcome { + val rs = str.split(", ").map(String::toInt) + return LitmusIIIOutcome(rs[0], rs[1], rs[2]) + } } fun LitmusOutcomeSpecScope.accept(r1: Int, r2: Int, r3: Int) = @@ -85,6 +97,10 @@ open class LitmusIIIIOutcome( } final override fun toList() = listOf(r1, r2, r3, r4) + final override fun parseOutcome(str: String): LitmusIIIIOutcome { + val rs = str.split(", ").map(String::toInt) + return LitmusIIIIOutcome(rs[0], rs[1], rs[2], rs[3]) + } } fun LitmusOutcomeSpecScope.accept(r1: Int, r2: Int, r3: Int, r4: Int) = diff --git a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LitmusAutoOutcome.kt b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LitmusAutoOutcome.kt index ce26e27..0b10855 100644 --- a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LitmusAutoOutcome.kt +++ b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LitmusAutoOutcome.kt @@ -25,5 +25,6 @@ sealed interface LitmusAutoOutcome { // for JCStress interop fun toList(): List + fun parseOutcome(str: String): LitmusAutoOutcome } diff --git a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LongAutoOutcomes.kt b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LongAutoOutcomes.kt index 4d5e759..fb1e7ac 100644 --- a/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LongAutoOutcomes.kt +++ b/core/src/commonMain/kotlin/org/jetbrains/litmuskt/autooutcomes/LongAutoOutcomes.kt @@ -13,6 +13,10 @@ open class LitmusLOutcome( } final override fun toList() = listOf(r1) + final override fun parseOutcome(str: String): LitmusLOutcome { + val rs = str.split(", ").map(String::toLong) + return LitmusLOutcome(rs[0]) + } } fun LitmusOutcomeSpecScope.accept(r1: Long) = @@ -36,6 +40,10 @@ open class LitmusLLOutcome( } final override fun toList() = listOf(r1, r2) + final override fun parseOutcome(str: String): LitmusLLOutcome { + val rs = str.split(", ").map(String::toLong) + return LitmusLLOutcome(rs[0], rs[1]) + } } fun LitmusOutcomeSpecScope.accept(r1: Long, r2: Long) = @@ -60,6 +68,10 @@ open class LitmusLLLOutcome( } final override fun toList() = listOf(r1, r2, r3) + final override fun parseOutcome(str: String): LitmusLLLOutcome { + val rs = str.split(", ").map(String::toLong) + return LitmusLLLOutcome(rs[0], rs[1], rs[2]) + } } fun LitmusOutcomeSpecScope.accept(r1: Long, r2: Long, r3: Long) = @@ -85,6 +97,10 @@ open class LitmusLLLLOutcome( } final override fun toList() = listOf(r1, r2, r3, r4) + final override fun parseOutcome(str: String): LitmusLLLLOutcome { + val rs = str.split(", ").map(String::toLong) + return LitmusLLLLOutcome(rs[0], rs[1], rs[2], rs[3]) + } } fun LitmusOutcomeSpecScope.accept(r1: Long, r2: Long, r3: Long, r4: Long) = diff --git a/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/Codegen.kt b/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/Codegen.kt index 79ce4fa..6f035ee 100644 --- a/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/Codegen.kt +++ b/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/Codegen.kt @@ -19,7 +19,7 @@ fun generateWrapperFile(test: LitmusTest<*>, generatedSrc: Path): Boolean { val targetCode = try { generateWrapperCode(test) } catch (e: Throwable) { - System.err.println("WARNING: could not generate wrapper for ${test.alias} because: ${e.message}") + System.err.println("WARNING: could not generate wrapper for ${test.alias} because:\n" + e.stackTraceToString()) return false } targetFile.writeText(targetCode) @@ -37,12 +37,15 @@ private fun generateWrapperCode(test: LitmusTest<*>): String { val outcomeTypeName = autoOutcomeClassList.first().simpleName!! .removePrefix("Litmus") .removeSuffix("Outcome") - val (outcomeVarType, outcomeVarCount) = when (outcomeTypeName) { - "I" -> "Integer" to 1 - "II" -> "Integer" to 2 - "III" -> "Integer" to 3 - "IIII" -> "Integer" to 4 - else -> error("unknown AutoOutcome type $outcomeTypeName") + + val outcomeVarTypes = outcomeTypeName.map { c -> + when (c) { + 'I' -> "Integer" + 'L' -> "Long" + 'Z' -> "Boolean" + // TODO: add others once they are created + else -> error("unrecognized outcome type '$c'") + } } val javaTestGetter: String = run { @@ -56,8 +59,8 @@ private fun generateWrapperCode(test: LitmusTest<*>): String { """ @Arbiter public void a($jcstressResultClassName r) { - List<$outcomeVarType> result = (List<$outcomeVarType>) (Object) ((LitmusAutoOutcome) fA.invoke(state)).toList(); - ${List(outcomeVarCount) { "r.r${it + 1} = result.get($it);" }.joinToString("\n ")} + List result = (List) (Object) ((LitmusAutoOutcome) fA.invoke(state)).toList(); + ${List(outcomeVarTypes.size) { "r.r${it + 1} = (${outcomeVarTypes[it]}) result.get($it);" }.joinToString("\n ")} } """.trim() } diff --git a/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/JCStressRunner.kt b/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/JCStressRunner.kt index 1c286b2..83a7f48 100644 --- a/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/JCStressRunner.kt +++ b/jcstress-wrapper/src/main/kotlin/org/jetbrains/litmuskt/JCStressRunner.kt @@ -1,5 +1,6 @@ package org.jetbrains.litmuskt +import org.jetbrains.litmuskt.autooutcomes.LitmusAutoOutcome import org.jetbrains.litmuskt.barriers.JvmCyclicBarrier import java.nio.file.Files import java.nio.file.Path @@ -41,7 +42,7 @@ class JCStressRunner( internal fun startTests( tests: List>, params: LitmusRunParams - ): () -> List { + ): () -> Map, LitmusResult> { val mvn = ProcessBuilder("mvn", "install", "verify", "-U") .directory(jcstressDirectory.toFile()) .redirectOutput(ProcessBuilder.Redirect.INHERIT) @@ -71,13 +72,17 @@ class JCStressRunner( return handle@{ jcs.waitFor() if (jcs.exitValue() != 0) error("jcstress exited with code ${jcs.exitValue()}") - return@handle tests.map { test -> parseJCStressResults(test) } + // not all tests might have generated wrappers + return@handle tests + .associateWith { test -> parseJCStressResults(test) } + .filterValues { it != null } + .mapValues { (_, result) -> result!! } // remove nullable type } } override fun startTest(test: LitmusTest, params: LitmusRunParams): () -> LitmusResult { val handle = startTests(listOf(test), params) - return { handle().first() } + return { handle()[test] ?: error("test $test did not produce a result; perhaps its wrapper is missing?") } } /** @@ -100,13 +105,11 @@ class JCStressRunner( * <-- these lines repeat per each configuration, so the results are summed in the end * ... */ - private fun parseJCStressResults(test: LitmusTest<*>): LitmusResult { + private fun parseJCStressResults(test: LitmusTest<*>): LitmusResult? { val resultsFile = jcstressDirectory / "results" / "${test.javaFQN}.html" + if (Files.notExists(resultsFile)) return null var lines = Files.lines(resultsFile).asSequence() - val allOutcomes = test.outcomeSpec.all - val outcomeStrings = allOutcomes.associateBy { it.toString().trim('(', ')') } - // get the number of observed outcomes lines = lines.dropWhile { !it.contains("Observed States") } val observedOutcomesLine = lines.splitFirst().let { (first, rest) -> lines = rest; first } @@ -115,9 +118,10 @@ class JCStressRunner( // skip to with outcomes lines = lines.drop(3) val linesOutcomes = lines.splitTake(observedSize).let { (first, rest) -> lines = rest; first } + val outcomeParser = test.stateProducer() as LitmusAutoOutcome val outcomesOrdered = linesOutcomes.map { val outcomeString = parseElementData(it) - outcomeStrings[outcomeString] ?: error("unrecognized outcome: $outcomeString") + outcomeParser.parseOutcome(outcomeString) }.toList() // lines with "bgColor" and "width" are the only ones with data @@ -142,7 +146,7 @@ class JCStressRunner( fun JCStressRunner.runTests( tests: List>, params: LitmusRunParams, -): List = startTests(tests, params).invoke() +): Map, LitmusResult> = startTests(tests, params).invoke() /** * Split a sequence into two: one with the first [size] elements and one with the rest.