Page MenuHomeIsabelle/Phabricator

Improve robustness of multithreaded Kodkod in Isabelle/Scala
Open, NormalPublic

Description

In Isabelle/0c7a74a1c6d9 enables option kodkod_scala (and auto_nitpick) by default. Thus nitpick invocations become more reactive, by reusing the already running Java process of Isabelle/Scala.

Occasional problems occur with isabelle build of Isabelle + AFP, with many parallel ML processes (e.g. -j8) sending tasks to the single managing Java process. In particular, situations of multithreaded Kodkod tasks (with interruption of parallel attempts?) seem to be prone to errors like this (seen e.g. in AFP/418c0aca9d53):

*** Unexpected outcome: "unknown"
*** At command "nitpick" (line 105 of "$AFP/Regular_Algebras/Regular_Algebras.thy")
*** Unexpected outcome: "unknown"
*** At command "nitpick" (line 101 of "$AFP/Regular_Algebras/Regular_Algebras.thy")

A temporary workaround is to switch batch sessions back to the old mode, where kodkod runs a heavy-weight Java process each time (in the session ROOT file):

options [kodkod_scala = false]

Event Timeline

makarius triaged this task as Normal priority.Oct 29 2020, 4:36 PM
makarius created this task.
makarius moved this task from TODO to Backlog on the isabelle-release board.

Disabled now (notably Isabelle2021-RC1), see Isabelle/6ead333e450d and AFP/2bccd7c8634c.

This requires to go through the Java implementation of Kodkod and SAT4j, and ensure that interrupts (or timeouts) are treated properly.

Back to external Java process for Isabelle2021-1 release (see 91ee232b4211).

Plan for the near future:

  • update from old Kodkod 1.5 to current version (e.g. 2.1)
  • proper treatment of interrupts in the Java implementation (also SAT4J!?)