From 5209289f27ba18a766c5fb8ac30eb7e961146a72 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 11 Jul 2022 18:35:27 -0400 Subject: [PATCH 1/3] Set a unique java.io.tmpdir for each call to SANY This should provide a workaround for the concurrency bug --- .../at/forsyte/apalache/tla/imp/SanyImporter.scala | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala index dbee7efac2..b2fb1372ab 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala @@ -68,8 +68,14 @@ class SanyImporter(sourceStore: SourceStore, annotationStore: AnnotationStore) e // Resolver for filenames, patched for wired modules. val filenameResolver = SanyNameToStream(libraryPaths) + // Set a unique tmpdir to avoid race-condition in SANY + // TODO: RM once https://github.com/tlaplus/tlaplus/issues/688 is fixed + // see + System.setProperty("java.io.tmpdir", sanyTempDir().toString()) + // call SANY val specObj = new SpecObj(file.getAbsolutePath, filenameResolver) + SANY.frontEndMain( specObj, file.getAbsolutePath, @@ -99,8 +105,7 @@ class SanyImporter(sourceStore: SourceStore, annotationStore: AnnotationStore) e * the pair (the root module name, a map of modules) */ def loadFromSource(source: Source, aux: Seq[Source] = Seq()): (String, Map[String, TlaModule]) = { - val tempDir = Files.createTempDirectory("sanyimp").toFile - + val tempDir = sanyTempDir() val nameAndModule = for { (rootName, rootFile) <- saveTlaFile(tempDir, source) // Save the aux modules to files, and get just the module names, if errors are hit, the first one will turn into a `Try` @@ -113,6 +118,9 @@ class SanyImporter(sourceStore: SourceStore, annotationStore: AnnotationStore) e nameAndModule.get } + // Create a unique temp directory for use by the SANY importer + private def sanyTempDir() = Files.createTempDirectory("sanyimp").toFile + private def ensureModuleNamesAreUnique(moduleNames: Seq[String]): Try[Unit] = { val duplicateNames = moduleNames.groupBy(identity).filter(_._2.size > 1) if (duplicateNames.isEmpty) { From b1e13e064927e1bca5e45be89348b99a158b00e7 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 12 Jul 2022 06:47:14 -0400 Subject: [PATCH 2/3] Update tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala Co-authored-by: Thomas Pani --- .../main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala | 1 - 1 file changed, 1 deletion(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala index b2fb1372ab..86e87460ce 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/SanyImporter.scala @@ -70,7 +70,6 @@ class SanyImporter(sourceStore: SourceStore, annotationStore: AnnotationStore) e // Set a unique tmpdir to avoid race-condition in SANY // TODO: RM once https://github.com/tlaplus/tlaplus/issues/688 is fixed - // see System.setProperty("java.io.tmpdir", sanyTempDir().toString()) // call SANY From 35e7ad2de7a4b965e22a749fc0544126414ca811 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 12 Jul 2022 07:06:24 -0400 Subject: [PATCH 3/3] Add changelog entry --- .unreleased/bug-fixes/1959-sany-tmpdir.md | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 .unreleased/bug-fixes/1959-sany-tmpdir.md diff --git a/.unreleased/bug-fixes/1959-sany-tmpdir.md b/.unreleased/bug-fixes/1959-sany-tmpdir.md new file mode 100644 index 0000000000..7daf6fb168 --- /dev/null +++ b/.unreleased/bug-fixes/1959-sany-tmpdir.md @@ -0,0 +1,2 @@ +Add workaround for Sany parsing failures when running parallel instances of +Apalache (see #1959)