diff options
| author | Enrico Tassi | 2014-11-28 18:41:43 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-28 18:41:43 +0100 |
| commit | 5d3f5c210aad8d73b007936e65694c401e66c7d0 (patch) | |
| tree | 2ec57168c42d7557ba27136722415e5288c7abd9 /dev/include | |
| parent | 9f4546a103607e0f2283897c094ce05ffa2d5c21 (diff) | |
STM: if a-p-always-delegate fetch states from parked worker on edit-at
If the async-proofs-always-delegate is passed, workers are killed
only when the proof they computed is obsolete. If one jumps back
to a state that was computed by the worker (and not the master) instead
of (re)computing such state in the master ask the worker to send it
back.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions