1 theory TimeLimit |
1 theory TimeLimit |
2 imports "../Appendix" |
2 imports "../Appendix" |
3 begin |
3 begin |
4 |
4 |
5 section {* Restricting the Runtime of a Function\label{rec:timeout} *} |
5 section {* Restricting the Runtime of a Function\label{rec:timeout} *} |
6 |
|
7 text {* |
6 text {* |
8 {\bf Problem:} |
7 {\bf Problem:} |
9 Your tool should run only a specified amount of time.\smallskip |
8 Your tool should run only a specified amount of time.\smallskip |
10 |
9 |
11 {\bf Solution:} In PolyML 5.2.1 and later, this can be achieved |
10 {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved |
12 using the function @{ML timeLimit in TimeLimit}.\smallskip |
11 using the function @{ML apply in Timeout}.\smallskip |
13 |
12 |
14 Assume you defined the Ackermann function on the ML-level. |
13 Assume you defined the Ackermann function on the ML-level. |
15 *} |
14 *} |
16 |
15 |
17 ML %grayML{*fun ackermann (0, n) = n + 1 |
16 ML %grayML{*fun ackermann (0, n) = n + 1 |
26 |
25 |
27 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
26 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
28 in a time limit of five seconds. For this you have to write |
27 in a time limit of five seconds. For this you have to write |
29 |
28 |
30 @{ML_response_fake_both [display,gray] |
29 @{ML_response_fake_both [display,gray] |
31 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
30 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) |
32 handle TimeLimit.TimeOut => ~1" |
31 handle TIMEOUT => ~1" |
33 "~1"} |
32 "~1"} |
34 |
33 |
35 where @{text TimeOut} is the exception raised when the time limit |
34 where @{text TimeOut} is the exception raised when the time limit |
36 is reached. |
35 is reached. |
37 |
36 |
38 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1 |
37 Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1 |
39 or later, because this version of PolyML has the infrastructure for multithreaded |
38 or later, because this version of PolyML has the infrastructure for multithreaded |
40 programming on which @{ML "timeLimit" in TimeLimit} relies. |
39 programming on which @{ML "apply" in Timeout} relies. |
41 |
40 |
42 \begin{readmore} |
41 \begin{readmore} |
43 The function @{ML "timeLimit" in TimeLimit} is defined in the structure |
42 The function @{ML "apply" in Timeout} is defined in the structure |
44 @{ML_struct TimeLimit} which can be found in the file |
43 @{ML_struct Timeout} which can be found in the file |
45 @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}. |
44 @{ML_file "Pure/concurrent/timeout.ML"}. |
46 \end{readmore} |
45 \end{readmore} |
47 |
46 |
48 |
47 |
49 *} |
48 *} |
50 end |
49 end |