1,735,192 research outputs found
On conservativity of concurrent Haskell
No full textThe 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
Clone Detection and Elimination for Haskell
No full textDuplicated code is a well known problem in software maintenance and refactoring. Code clones tend to increase program size and several studies have shown that duplicated code makes maintenance and code understanding more complex and time consuming. This paper presents a new technique for the detection and removal of duplicated Haskell code. The system is implemented within the refactoring framework of the Haskell Refactorer (HaRe), and uses an Abstract Syntax Tree (AST) based approach. Detection of duplicate code is automatic, while elimination is semi-automatic, with the user managing the clone removal. After presenting the system, an example is given to show how it works in practice
Realising nondeterministic I/O in the Glasgow Haskell Compiler
No full textIn this paper we demonstrate how to relate the semantics given by the nondeterministic call-by-need calculus FUNDIO [SS03] to Haskell. After introducing new correct program transformations for FUNDIO, we translate the core language used in the Glasgow Haskell Compiler into the FUNDIO language, where the IO construct of FUNDIO corresponds to direct-call IO-actions in Haskell. We sketch the investigations of [Sab03b] where a lot of program transformations performed by the compiler have been shown to be correct w.r.t. the FUNDIO semantics. This enabled us to achieve a FUNDIO-compatible Haskell-compiler, by turning o not yet investigated transformations and the small set of incompatible transformations. With this compiler, Haskell programs which use the extension unsafePerformIO in arbitrary contexts, can be compiled in a "safe" manner
Combinators for Message-Passing in Haskell
No full textMuch code in message-passing programs is tedious, verbose wiring code. This code is error prone and laborious - and tends to be repeated across many programs with only slight variations. By using type-classes, higher-order and monadic functions in Haskell, most of this code can be captured in re-usable high-level combinators that shorten and simplify message-passing programs. We motivate the design and use of these combinators via an example of a concurrent biological simulation, and explain their implementation in the Communicating Haskell Processes library
Practical Verification of Concurrent Haskell Programs
No full textThe formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error, this paper investigates how Agda2hs can be used to automate the verification process in Agda, while keeping the advantages of having our code available in Haskell. This paper shows how Agda2hs enables the partial verification of a simple Haskell concurrency model. The model is first ported to Agda, staying as close to the original code as possible, and directly compared to the Haskell translation provided by Agda2hs to showcase the readability of the code it produces. Consequently, it is shown how Agda's proof techniques can be used to provide straightforwards proofs of the presence or absence of deadlocks in simple concurrent programs written in this model. Finally, the model's limitations, in particular its deterministic nature, are discussed.https://github.com/mschifferstein/concurrent-haskell-verification Github repositoryCSE3000 Research ProjectComputer Science and Engineerin
Formalisation of Haskell Refactorings
No full textRefactoring is a well-known technique for improving the design of existing programs without changing their external behaviour. HaRe is the refactoring tool we have built to support refactoring Haskell programs. Along with the development of HaRe, This formalisation process helps to clarify the meaning of refactorings, improves our confidence in the behaviour-preservation of refactorings, and reduces the need for testing. This paper gives an overview of HaRe, and shows our approach to the formalisation of refactorings
Communicating Haskell Processes
No full textConcurrent programming supports multiple threads of concurrent execution. It
is a suitable paradigm for interaction with the outside world, where many inputs
(e.g. network packets, key-presses, mouse-clicks) may arrive at any time and need
to be dealt with at the same time. Concurrent execution also potentially allows
for parallel speed-up; multicore machines are now the standard for new PCs, but
the quest to take full advantage of the available parallelism continues.
One approach to concurrent programming is process-oriented programming,
which uses message-passing and is based on Hoare and Roscoe's Communicating
Sequential Processes (CSP). CSP is a process calculus centred on concurrent processes that communicate with each other via synchronous channels. This is used
as a formal underpinning for process-oriented programming, either directly (proving behaviours of programs with a CSP model checker) or indirectly (providing
sound design principles and patterns).
Process-oriented programming has previously been provided in programming
languages such as occam-? and libraries for other mainstream languages such as
Java and C++. However, as yet process-oriented programming has failed to gain
much traction via these implementations; occam-? is rooted in the much older
language occam and thus lacks powerful data structures (among other features)
which are standard in most modern languages { while languages such as Java
and C++, where data is mutable and easily shared, can be an awkward fit to
process-oriented programming.
Haskell is a functional programming language that is notable for its purity,
type-classes, monads and lazy evaluation: modern features that provide interest-
ing and powerful ways to program, including good support for imperative pro-
gramming. Like other functional languages, it eliminates mutable data -- which
immediately removes a whole class of problems in concurrent programming.
This thesis contends that CSP and process-oriented programming ?t well with
Haskell. The thesis details the creation of a CSP library for Haskell (Commu-
nicating Haskell Processes: CHP) { which features powerful support for process
composition { and its further augmentation with capabilities such as support for
a new concurrency primitive (conjunction), tracing and the ability to generate
formal models of CHP programs. This allows programmers to build concurrent
message-passing systems with a strong formal underpinning in a modern program-
ming language, with more features and less complications than process-oriented
libraries for other languages
Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack
No full textExisting algorithmic debuggers for Haskell require a transformation of all modules in a program, even libraries that the user does not want to debug and which may use language features not supported by the debugger. This is a pity, because a promising ap- proach to debugging is therefore not applicable to many real-world programs. We use the cost centre stack from the Glasgow Haskell Compiler profiling environment together with runtime value observations as provided by the Haskell Object Observation Debugger (HOOD) to collect enough information for algorithmic debugging. Program annotations are in suspected modules only. With this technique algorithmic debugging is applicable to a much larger set of Haskell programs. This demonstrates that for functional languages in general a simple stack trace extension is useful to support tasks such as profiling and debugging
Automatically Generating CSP Models for Communicating Haskell Processes
No full textTools such as FDR can check whether a CSP model of an implementation is a refinement of a given CSP specification. We present a technique for generating such CSP models of Haskell implementations that use the Communicating Haskell Processes library. Our technique avoids the need for a detailed semantics of
the Haskell language, and requires only minimal program annotation. The generated CSP-M model can be checked for deadlock or refinements by FDR, allowing easy use of formal methods without the need to maintain a model of the program implementation alongside the program itself
Software Metrics: Measuring Haskell
No full textSoftware metrics have been used in software engineering as a mechanism for assessing code quality and for targeting software development activities, such as testing or refactoring, at areas of a program that will most benefit from them. Haskell has many tools for software engineering, such as testing, debugging and refactoring tools, but software metrics have mostly been neglected. The work presented in this paper identifies a collection of software metrics for use with Haskell programs. These metrics are subjected to statistical analysis to assess the correlation between their values and the number of bug fixing changes occurring during the development lifetime of two case study programs. In addition to this, the relationships between the metric values is also explored, showing how combinations of metrics can be used to improve the accuracy of the measurements
- …
