Difference between revisions of "Concurrency with oracles"
(Attempt to improve clarity of description...) |
m (More corrections >_<) |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | == Oracles, defined == |
||
| + | == The problem == |
||
| − | An ''oracle'' is a value that can be viewed as having the ability to predict e.g: |
||
| + | While there has been research into ''deterministic'' concurrency (e.g. Eleni Spiliopoulou's work with the Bristol Haskell system as described in his thesis [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.60.4364&rep=rep1&type=pdf Concurrent and Distributed Functional Systems]), models of concurrency are generally ''nondeterministic''. For programming languages like Haskell which have the goal of being [[Referential transparency|referentially transparent]], the nondeterminism associated with concurrency presents a challenge - the usual techniques for supporting it used by most other (imperative) languages cannot not be simply transferred verbatim. |
||
| + | |||
| + | But neither can nondeterminism be just ignored - to quote F. Warren Burton from [https://academic.oup.com/comjnl/article-pdf/31/3/243/1157325/310243.pdf Nondeterminism with Referential Transparency in Functional Programming Languages]: |
||
| + | |||
| + | <i><blockquote> |
||
| + | Nondeterminism is useful in real-time applications where the behaviour of a program should depend on the order in which external events occur. For example, it might be desirable to merge the elements of two lists in the order in which the elements become available. This type of nondeterminism appears to be necessary if functional programs are to be used for real-time computing. |
||
| + | </blockquote></i> |
||
| + | |||
| + | Other example include: |
||
* which out of two computations will finish first; |
* which out of two computations will finish first; |
||
* which input event will arrive first; |
* which input event will arrive first; |
||
* whether a computation will finish before an input event arrives. |
* whether a computation will finish before an input event arrives. |
||
| + | For concurrent programs, nondeterminism is inescapable - events like storage, network or other external failures can occur without warning. The languages used for writing such programs must have some way to allow these programs to cope with such degradation gracefully while continuing to carry out the majority of their designated tasks, albeit at reduced capacity. |
||
| − | In practice this apparent predictive power is the result of the measured use of outside information (possibly as a result of external effects). The oracle, by seeming to contain the prediction, will preserve the [[Referential transparency|referential transparency]] of a language while allowing expression of computations whose outcomes depend on execution time and arrival time. |
||
| + | == How oracles can help == |
||
| − | Solutions tend to involve infinite trees of oracles, so you can pull one out whenever you need one, and pass an infinite subtree to future computations. Of course once an oracle has been used, it can't be reused. [[Referential transparency]] demands that the outcome of applying the oracle is fixed. |
||
| + | By presenting them to programs via a (theoretically) infinite structured value such as a tree, [[Opting for oracles|oracles]] allow for the controlled use of nondeterminism while maintaining referential transparency - wherever the program requires an nondeterministic result, an oracle is then used for this purpose through the use of operations from the interface for the corresponding abstract data type. Once an oracle has been used, it can't be reused - referential transparency demands that the outcome of applying the oracle remains constant. |
||
| − | == |
+ | == Examples of use == |
| + | K. V. S. Prasad uses oracles directly in ''A Calculus of Broadcasting Systems''; Peter Dybjer, Herbert Sander and Mieke Massink use the concept for reasoning about various models of concurrency and their possible applications. |
||
| − | |||
| − | On page 32 of 60 in ''Tackling the Awkward Squad'', Simon Peyton Jones introduces non-determinism as a result of adding concurrency to the ''operational semantics'' he provides for I/O. As shown by |
||
| − | Peter Dybjer, Herbert Sander and Mieke Massink, the throughtful use of oracles can help to recover |
||
| − | referential transparency in models of concurrency despite them being non-deterministic. |
||
== References == |
== References == |
||
| − | |||
* [http://www.cse.chalmers.se/~peterd/papers/FACS1989.pdf A Functional Programming Approach to the Specification and Verification of Concurrent Systems], Peter Dybjer and Herbert Sander. |
* [http://www.cse.chalmers.se/~peterd/papers/FACS1989.pdf A Functional Programming Approach to the Specification and Verification of Concurrent Systems], Peter Dybjer and Herbert Sander. |
||
* [https://www.ru.nl/publish/pages/682191/massinkm.pdf Functional Techniques in Concurrency], Mieke Massink. |
* [https://www.ru.nl/publish/pages/682191/massinkm.pdf Functional Techniques in Concurrency], Mieke Massink. |
||
| − | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1. |
+ | * [https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.6225&rep=rep1&type=pdf A Calculus of Broadcasting Systems], K. V. S. Prasad. |
[[Category:Concurrency]] |
[[Category:Concurrency]] |
||
Revision as of 22:38, 22 March 2021
The problem
While there has been research into deterministic concurrency (e.g. Eleni Spiliopoulou's work with the Bristol Haskell system as described in his thesis Concurrent and Distributed Functional Systems), models of concurrency are generally nondeterministic. For programming languages like Haskell which have the goal of being referentially transparent, the nondeterminism associated with concurrency presents a challenge - the usual techniques for supporting it used by most other (imperative) languages cannot not be simply transferred verbatim.
But neither can nondeterminism be just ignored - to quote F. Warren Burton from Nondeterminism with Referential Transparency in Functional Programming Languages:
Nondeterminism is useful in real-time applications where the behaviour of a program should depend on the order in which external events occur. For example, it might be desirable to merge the elements of two lists in the order in which the elements become available. This type of nondeterminism appears to be necessary if functional programs are to be used for real-time computing.
Other example include:
- which out of two computations will finish first;
- which input event will arrive first;
- whether a computation will finish before an input event arrives.
For concurrent programs, nondeterminism is inescapable - events like storage, network or other external failures can occur without warning. The languages used for writing such programs must have some way to allow these programs to cope with such degradation gracefully while continuing to carry out the majority of their designated tasks, albeit at reduced capacity.
How oracles can help
By presenting them to programs via a (theoretically) infinite structured value such as a tree, oracles allow for the controlled use of nondeterminism while maintaining referential transparency - wherever the program requires an nondeterministic result, an oracle is then used for this purpose through the use of operations from the interface for the corresponding abstract data type. Once an oracle has been used, it can't be reused - referential transparency demands that the outcome of applying the oracle remains constant.
Examples of use
K. V. S. Prasad uses oracles directly in A Calculus of Broadcasting Systems; Peter Dybjer, Herbert Sander and Mieke Massink use the concept for reasoning about various models of concurrency and their possible applications.
References
- A Functional Programming Approach to the Specification and Verification of Concurrent Systems, Peter Dybjer and Herbert Sander.
- Functional Techniques in Concurrency, Mieke Massink.
- A Calculus of Broadcasting Systems, K. V. S. Prasad.