|
2 | 2 | Simulate a multi-threaded program that has been |
3 | 3 | instrumented to save traces of its API calls in a log. |
4 | 4 |
|
5 | | -Demonstrate the nondeterminism in the order in which API calls and |
6 | | -returns are made, and the order they appear in the trace log. |
| 5 | +Instead of simply calling the API functions, each thread instead calls |
| 6 | +the *tracecapture* function, which calls the API function but also |
| 7 | +saves the call (with arguments) and return (with return value) in the |
| 8 | +trace log. The tracecapture function uses a lock: |
| 9 | +
|
| 10 | + tracelock = lock() |
| 11 | +
|
| 12 | + tracecapture(thread_id, call, args): # call is action name |
| 13 | + tracelock.acquire() |
| 14 | + log(thread_id, call, "start", args) # log the call with arguments |
| 15 | + tracelock.release() # release here allows threads to interleave |
| 16 | + ret = call(*args) |
| 17 | + tracelock.acquire() |
| 18 | + log(thread_id, call, "finish", ret) # log the return with return value |
| 19 | + tracelock.release() |
| 20 | + return ret |
| 21 | +
|
| 22 | +The purpose of *tracelock* is to ensure that only one thread at a time |
| 23 | +can write to the trace log. To allow threads to interleave, the first |
| 24 | +*tracelock.release()* *precedes* the call, otherwise the call might |
| 25 | +block and hold *tracelock*, prevent other threads from running while |
| 26 | +that call blocks. |
| 27 | +
|
| 28 | +This model program Demonstrates the nondeterminism in the order in |
| 29 | +which API calls and returns are made, and the order they appear in the |
| 30 | +trace log. |
7 | 31 |
|
8 | 32 | Parameters (constants that do not change when the model executes): |
9 | 33 |
|
|
17 | 41 | Indicates which action in program each thread is executing |
18 | 42 |
|
19 | 43 | phase: phase of each thread, indexed by thread id |
20 | | -models progress through the tracecapture function (see README) |
| 44 | +models progress through the tracecapture function (see above) |
21 | 45 | For each API call in program, phases in order are: ready, start, call, finish |
22 | 46 | phase[thread] == start means thread holds tracelock to write call start |
23 | 47 | phase[thread] == finish means thread holds tracelock to write call finish |
|
0 commit comments