[isabelle] Troubleshooting a nondeterministic SMT failure · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Troubleshooting a nondeterministic SMT failure

Email Gateway (Nov 18 2021 at 11:00):

From: Brandon Bohrer <bjbohrer@gmail.com>
Hi all,

Short version: I am getting failures in the "smt" method,
nondeterministically on the released version of an AFP article
(Poincare-Bendixson); what troubleshooting steps are recommended next?

Since I have already taken some troubleshooting steps, the rest of my email
describes what I have tried already, to help speed up troubleshooting. Note
that I have one machine with the problem and one without it, which may help.

Failing command (for example):
$ isabelle build -d <path-to-afp>/thys -b Poincare_Bendixson

Isabelle version: Tried 2019 and 2021 with matching AFP versions. No change.

Machine & OS information:
I have tested this on two machines, call them machine W (where the proof
works) and machine B (where it's broken). Both run Windows 10. Both use the
built-in Windows antivirus and I am prevented from turning it off
completely, but I have added exclusions for my Isabelle and AFP
directories. Also turned off search indexing of file contents.

The first difference between the machines that comes to mind: machine W is
newer and faster; it has both an SSD and an HDD. However, I moved Isabelle
(including .isabelle) and the AFP to my HDD, and the issue persisted. I
still wonder whether Windows is using the SSD without my knowing, and
racing.

Solvers: I tried Z3, CVC4, and VeriT. No change.

Timing and nondeterminism:
It is definitely nondeterministic. If I rerun an offending line through the
jEdit UI, it usually works on a second or third try. Whether it succeeds or
fails, it always returns quickly (e.g. 0.2 seconds for one of them). So it
is not a timeout issue.

SMT tracing information:
I enabled the smt_trace option and noticed something: When "smt" fails, the
"SMT: Result:" message doesn't have any, well, results after it, but when
"smt" succeeds, there is lots of trace info. Is this expected behavior or
is it a clue about what's going wrong? I can rerun and post the whole trace
if needed.

Thanks for any advice you can provide!

Brandon Bohrer
Assistant Professor of Computer Science
Worcester Polytechnic Institute

Email Gateway (Nov 18 2021 at 12:18):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Brandon,

The most likely problem is that the thread launching the SMT solver is not
started fast enough. Set the timeout to infinity with declare [[smt_timeout=0]] should do the trick (this is the default value in
Isabelle2021-1-RC3 anyway).

Best,
Mathias

Email Gateway (Nov 18 2021 at 14:31):

From: Brandon Bohrer <bjbohrer@gmail.com>
Hi Mathias,

Thanks for the quick reply. I actually have already tried setting high
timeouts as well (e.g. declare[[smt_timeout=10000]]) but did not mention
that explicitly in my first email because all of the successful smt calls
and all of the failing smt calls complete quite quickly (e.g. 0.2 seconds).
Note that things are failing on my faster machine and succeeding on my
slower machine.

By the way, I also tried declare[[smt_timeout=0]] right now, just in case
(on the Isabelle2021 release, not an RC). The result was that it set the
timeout to 0 seconds rather than infinity, so that all of the smt calls
fail every time. At least that's a deterministic behavior, so maybe it's an
improvement :)

Let me know if there are any other troubleshooting steps that I should try
next, or if there is any additional debug info that would be helpful to
post to the list.

Thanks!
-Brandon

Email Gateway (Nov 20 2021 at 11:46):

From: Makarius <makarius@sketis.net>
The smt_timeout behaviour changed shortly after the Isabelle2021 release, so
in Isabelle2021-1 release candidates it observes the common scheme of Isabelle
tools that 0 means infinity (actually anything < 1ms).

Email Gateway (Nov 22 2021 at 15:28):

From: Brandon Bohrer <bjbohrer@gmail.com>
Dear Makarius,

Thanks for the follow-up, that definitely clears up my misunderstanding of
Mathias' earlier email. I don't have any of the RCs installed at the
moment, but if I'm reading the news correctly, I expect that my original
issue would be unchanged if I run an RC.

Changing timeouts was one of the troubleshooting steps I tried and timeouts
did not appear to be the issue. Since I'm on the 2021 release, I set the
timeout to 10000 seconds (~2 hours) rather than setting the value to 0, and
the SMT calls in question finished in well under a second, both the
successful and unsuccessful calls. No timeouts occur on the default
setting, nor when I increase the timeout limit.

Taking that into consideration, I would be happy to hear from anyone
whether it makes sense to install and test an RC (or nightly) build. For
example, if there are major SMT communication protocol changes other that
the timeout handling, then I think testing the latest version would still
make sense.

Thanks again everyone for the troubleshooting help,
-Brandon

Last updated: Jul 15 2022 at 23:21 UTC