search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
67 stars 20 forks source link

Solver timeout isn't respected properly #53

Open will62794 opened 3 years ago

will62794 commented 3 years ago

When using the --stretch parameter of tlapm, the resulting timeouts for the backend solvers don't seem to respected properly. See the following output from the attached repro (tlapm-timeout-repro.zip):

$ tlapm --toolbox 0 0  --printallobs --debug tempfiles --method smt --cleanfp --stretch 0.1 MongoRaftReconfig_TautCheck.tla

\* TLAPM version 1.4.5 (commit 33809)
\* launched at 2021-10-29 00:00:33 with command line:
\* tlapm --toolbox 0 0 --printallobs --debug tempfiles --method smt --cleanfp --stretch 0.1 MongoRaftReconfig_TautCheck.tla

(* fingerprints file "MongoRaftReconfig_TautCheck.tlaps/fingerprints" removed *)
@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:6:15:6:22
@!!status:to be proved
@!!obl:ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  TRUE

@!!END

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:5:23:5:25
@!!status:to be proved
@!!obl:ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion,
       Inv1 ==
         \A i, j \in Server :
            configTerm[i] =< configTerm[j]
            \/ (configTerm[i] = configTerm[j]
                \/ (~IsNewerOrEqualConfig(j, i) /\ TRUE))
PROVE  Inv1 <=> TRUE

@!!END

@!!BEGIN
@!!type:obligationsnumber
@!!count:2
@!!END

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:6:15:6:22
@!!status:normalized
@!!meth:time-limit: 0.5
@!!obl:ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  TRUE

@!!END

** Unexpanded symbols: ---

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:5:23:5:25
@!!status:normalized
@!!meth:time-limit: 0.5
@!!obl:ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  (\A i, j \in Server :
           configTerm[i] =< configTerm[j]
           \/ (configTerm[i] = configTerm[j]
               \/ (~IsNewerOrEqualConfig(j, i) /\ TRUE)))
       <=> TRUE

@!!END

** Unexpanded symbols: IsNewerOrEqualConfig

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:6:15:6:22
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 0.5; time-used: 0.1 (19%)
@!!already:false
@!!obl:
ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  TRUE

@!!END

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:5:23:5:25
@!!status:being proved
@!!prover:smt
@!!meth:time-limit: 0.5
@!!obl:
ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  (\A i, j \in Server :
           configTerm[i] =< configTerm[j]
           \/ (configTerm[i] = configTerm[j]
               \/ (~IsNewerOrEqualConfig(j, i) /\ TRUE)))
       <=> TRUE

@!!END

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:5:23:5:25
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 0.5; time-used: 3.0 (601%)
@!!reason:timeout
@!!already:false
@!!obl:
ASSUME NEW CONSTANT Server,
       NEW CONSTANT Secondary,
       NEW CONSTANT Primary,
       NEW CONSTANT Nil,
       NEW CONSTANT InitTerm,
       NEW VARIABLE log,
       NEW VARIABLE committed,
       NEW VARIABLE currentTerm,
       NEW VARIABLE state,
       NEW VARIABLE config,
       NEW VARIABLE configVersion,
       NEW VARIABLE configTerm,
       NEW VARIABLE elections,
       NEW CONSTANT MaxTerm,
       NEW CONSTANT MaxLogLen,
       NEW CONSTANT MaxConfigVersion
PROVE  (\A i, j \in Server :
           configTerm[i] =< configTerm[j]
           \/ (configTerm[i] = configTerm[j]
               \/ (~IsNewerOrEqualConfig(j, i) /\ TRUE)))
       <=> TRUE

@!!END

(* created new "MongoRaftReconfig_TautCheck.tlaps/MongoRaftReconfig_TautCheck.thy" *)
(* fingerprints written in "MongoRaftReconfig_TautCheck.tlaps/fingerprints" *)

The last obligation status message printed reports the following:

@!!meth:time-limit: 0.5; time-used: 3.0 (601%)

which seems that it violated the allowed timeout budget. My understanding is that Z3, for example, can directly handle millisecond timeout values e.g.

$ z3 -h
Z3 [version 4.8.10 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
Usage: z3 [options] [-file:]file
...
Resources:
  -T:timeout  set the timeout (in seconds).
  -t:timeout  set the soft timeout (in milli seconds). It only kills the current query.
  -memory:Megabytes  set a limit for virtual memory consumption.

so it's unclear why this timeout is not being respected properly

will62794 commented 3 years ago

Note: When using Z3 as a backend solver, I believe this can be worked around by manually specifying a timeout in the Z3 arguments e.g. giving a timeout of 100 milliseconds:

tlapm --toolbox 0 0  --printallobs --debug tempfiles --method smt --solver 'z3 -t:100 -smt2 "$file"' --nofp --stretch 0.1 MongoRaftReconfig_TautCheck.tla