Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected Behavior with Isabelle Server 2023

Email Gateway (Jan 08 2024 at 09:44):

From: "Joshua K." <j.kobschaetzki@campus.tu-berlin.de>
Hi,

I've recently started working on writing a k6[^0] adapter[^1] for
stress-testing a server compatible with the isabelle server protocol.
The main purpose of the adapter is to analyze the performance
characteristics and behavior of Isabelle server with multiple users and
sessions. During the initial testing phase, I encountered some
unexpected behavior related to the session_stop command. It seems to
trigger a race-condition or edge case, especially when called in quick
succession after start_session, use_theories, and purge_theories[^2] in
a loop. Typically, this occurs on the second to fourth iteration.

Here are the observed stack traces from the Isabelle server's stdout:

observed with a single user:

Exception in thread "event_timer"
*** Inactive prover input thread for command
"Document.discontinue_execution"
   at isabelle.Exn$ERROR$.apply(exn.scala:25)
   at isabelle.Exn$.error(exn.scala:29)
   at isabelle.package$.$init$$$anonfun$1(ROOT.scala:9)
   at isabelle.Prover.protocol_command_raw(prover.scala:296)
   at isabelle.Prover.protocol_command_args(prover.scala:301)
   at isabelle.Prover.protocol_command(prover.scala:305)
   at isabelle.Protocol.discontinue_execution(protocol.scala:395)
   at isabelle.Protocol.discontinue_execution$(protocol.scala:306)
   at isabelle.Prover.discontinue_execution(prover.scala:71)
   at isabelle.Session.handle_raw_edits$1(session.scala:397)
   at isabelle.Session.$init$$$anonfun$3(session.scala:648)
   at
isabelle.Consumer_Thread$.consume_single$1$$anonfun$1(consumer_thread.scala:28)
   at isabelle.Exn$.capture(exn.scala:60)
   at isabelle.Consumer_Thread$.consume_single$1(consumer_thread.scala:28)
   at isabelle.Consumer_Thread$.fork$$anonfun$2(consumer_thread.scala:34)
   at isabelle.Consumer_Thread.process(consumer_thread.scala:90)
   at isabelle.Consumer_Thread.main_loop(consumer_thread.scala:108)
   at isabelle.Consumer_Thread.$init$$$anonfun$1(consumer_thread.scala:50)
   at
isabelle.Consumer_Thread.$init$$$anonfun$adapted$1(consumer_thread.scala:50)
   at scala.Function0.apply$mcV$sp(Function0.scala:42)
   at isabelle.Isabelle_Thread$.$anonfun$2(isabelle_thread.scala:64)
   at isabelle.Isabelle_Thread.run(isabelle_thread.scala:140)

Also observed, but only when concurrently applying the same commands
with 2 or more "users":

Exception in thread "event_timer"
*** Consumer thread not active: "Isabelle.Session.manager"
   at isabelle.Exn$ERROR$.apply(exn.scala:25)
   at isabelle.Exn$.error(exn.scala:29)
   at isabelle.package$.$init$$$anonfun$1(ROOT.scala:9)
   at isabelle.Consumer_Thread.request(consumer_thread.scala:78)
   at isabelle.Consumer_Thread.send_wait(consumer_thread.scala:118)
   at isabelle.Session.update(session.scala:760)
   at
isabelle.Headless$Resources.load_theories$$anonfun$1(headless.scala:675)
   at isabelle.Synchronized.change(synchronized.scala:67)
   at isabelle.Headless$Resources.load_theories(headless.scala:676)
   at
isabelle.Headless$Session.check_state$1$$anonfun$3(headless.scala:338)
   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
   at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
   at scala.Option$WithFilter.foreach(Option.scala:437)
   at isabelle.Headless$Session.check_state$1(headless.scala:338)
   at
isabelle.Headless$Session.check_progress$lzyINIT1$1$$anonfun$1(headless.scala:347)
   at
isabelle.Headless$Session.check_progress$lzyINIT1$1$$anonfun$adapted$1(headless.scala:349)
   at scala.Function0.apply$mcV$sp(Function0.scala:42)
   at isabelle.Event_Timer$$anon$1.run(event_timer.scala:28)
   at java.base/java.util.TimerThread.mainLoop(Timer.java:566)
   at java.base/java.util.TimerThread.run(Timer.java:516)

Interestingly, during testing, the specific theory for use_theories
didn't seem to affect the outcome.

However, the exception doesn't occur if a delay of >2-3 seconds is
inserted between session_stop and use_theories calls. This led me to
suspect a race condition, but I couldn't pinpoint the exact cause in the
Server code.

I would greatly appreciate any advice or guidance on how to address this
behavior. Is there a way to navigate the timer issues without resorting
to delaying the execution on the client?

Best regards,
Joshua Kobschätzki

[^0]: https://k6.io/open-source/

[^1]: https://git.tu-berlin.de/cobalt.rocks/isa-bench, a MRE, if
requested, can be made available

[^2]: Command log -- executed after successful client<>server handshake:

executed in a loop -- exception occurred at 2-4 iteration

session_start {"session": "HOL", "options":
["headless_consolidate_delay=0.5", "headless_prune_delay=5",
"show_states"]}\n

await session start, retrieve session id

use_theories {"session_id": "{{ previously retrieved session id }}",
"theories": ["{{ some theory, the specific theory didn't matter during
testing }}"], "master_dir": "{{ theory path }}"}\n

await use_theories

purge_theories {"session_id": "{{ previously retrieved session id }}",
"all": true}\n

await purge_theories

session_stop {"session_id": "{{ previously retrieved session id }}"}\n

await session_stop, if exception occurs:

FAILED {"kind": "error", "message": "java.lang.IllegalStateException:

Timer already cancelled.","task": "<task id for session_close>"}

the stack trace will be dispalyed in the corresponding server stdout

Last updated: Apr 29 2024 at 01:08 UTC