closes#1134
see #1362
This feature is implemented using a "hearbeat" thread local counter.
We reset the counter whenever we start a new task.
The counter is incremented when:
1- An object is allocated using small_object_allocator (e.g., VM object)
2- An object is allocated using memory_pool (e.g., expr, level, rb_tree nodes, list cons-cells, etc)
3- check_system(...) invocations
We check if the threshold was reached at check_system.
The option --timeout=num can be used to set the limit (in thousands).
The default is unbounded in batch mode.
In server mode, the default is 100000. We can compile the standard library with --timeout=12000
I did not perform many experiments to check how precise this counter is.
I added a new Emacs configuration setting to change the server default.
Here is the wall clock time for different values of --timeout for the
command used on issue #1134
time ../../bin/lean -j 0 --timeout=20000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.070s
user 0m1.032s
sys 0m0.036s
time ../../bin/lean -j 0 --timeout=40000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.777s
user 0m1.676s
sys 0m0.044s
time ../../bin/lean -j 0 --timeout=50000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.985s
user 0m1.920s
sys 0m0.056s
time ../../bin/lean -j 0 --timeout=100000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m3.587s
user 0m3.564s
sys 0m0.020s
This commit allows us to build Lean without the pthread dependency.
It is also useful if we want to implement multi-threading on top of Boost.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.
The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:
try-for (T1 ORELSE T2) 5
It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
