OPUS 4 Latest Documents RSS FeedLatest documents
http://publikationen.ub.uni-frankfurt.de/index/index/
Thu, 07 Aug 2014 14:12:40 +0200Thu, 07 Aug 2014 14:12:40 +0200On correctness of buffer implementations in a concurrent lambda calculus with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34435
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34435Tue, 08 Jul 2014 14:12:40 +0200On conservativity of concurrent Haskell
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34312
The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus which comprises data constructors, case-expressions, letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity of CHF, that is, all equivalences of pure functional expressions are also valid in CHF. This implies that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that this is no longer valid if Concurrent Haskell is extended by the arbitrary use of unsafeInterleaveIO.David Sabel; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34312Thu, 03 Jul 2014 14:49:03 +0200On conservativity of concurrent Haskell
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24252
The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus which comprises data constructors, case-expressions, letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity of CHF, that is, all equivalences of pure functional expressions are also valid in CHF. This implies that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that this is no longer valid if Concurrent Haskell is extended by the arbitrary use of unsafeInterleaveIO.David Sabel; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24252Tue, 07 Feb 2012 16:16:23 +0100An abstract machine for concurrent Haskell with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24253
We show how Sestoft’s abstract machine for lazy evaluation of purely functional programs can be extended to evaluate expressions of the calculus CHF – a process calculus that models Concurrent Haskell extended by imperative and implicit futures. The abstract machine is modularly constructed by first adding monadic IO-actions to the machine and then in a second step we add concurrency. Our main result is that the abstract machine coincides with the original operational semantics of CHF, w.r.t. may- and should-convergence.David Sabelworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/24253Tue, 07 Feb 2012 16:14:01 +0100On correctness of buffer implementations in a concurrent lambda calculus with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schaußworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/6666Tue, 07 Jul 2009 13:22:26 +0200Program equivalence for a concurrent lambda calculus with futures
http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2181
Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures Lambda(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics.Joachim Niehren; David Sabel; Manfred Schmidt-Schauß; Jan Schwinghammerworkingpaperhttp://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2181Mon, 30 Oct 2006 08:54:30 +0100