| 1. |
|
|
| 2. |
- Aronsson, Markus, 1990, et al.
(författare)
-
Hardware software co-design in Haskell
- 2017
-
Ingår i: Haskell 2017 - Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2017. - New York, NY, USA : ACM. ; 52:10, s. 162-173
-
Konferensbidrag (refereegranskat)abstract
- We present a library in Haskell for programming Field Programmable Gate Arrays (FPGAs), including hardware software co-design. Code for software (in C) and hardware (in VHDL) is generated from a single program, along with the code to support communication between hardware and software. We present type-based techniques for the simultaneous implementation of more than one embedded domain specific language (EDSL). We build upon a generic representation of imperative programs that is loosely coupled to instruction and expression types, allowing the individual parts to be developed and improved separately. Code generation is implemented as a series of translations between progressively smaller, typed EDSLs, safeguarding against errors that arise in untyped translations. Initial case studies show promising performance.
|
|
| 3. |
- Bardizbanyan, Alen, 1986, et al.
(författare)
-
Improving data access efficiency by using context-aware loads and stores
- 2015
-
Ingår i: Proc. 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. - New York : ACM Press. - 0730-8566. - 9781450332576 ; , s. 27-36
-
Konferensbidrag (refereegranskat)abstract
- Memory operations have a significant impact on both performance and energy usage even when an access hits in the level-one data cache (L1 DC). Load instructions in particular affect performance as they frequently result in stalls since the register to be loaded is often referenced before the data is available in the pipeline. L1 DC accesses also impact energy usage as they typically require significantly more energy than a register file access. Despite their impact on performance and energy usage, L1 DC accesses on most processors are performed in a general fashion without regard to the context in which the load or store operation is performed. We describe a set of techniques where the compiler enhances load and store instructions so that they can be executed with fewer stalls and/or enable the L1 DC to be accessed in a more energy-efficient manner. We show that using these techniques can simultaneously achieve a 6% gain in performance and a 43% reduction in L1 DC energy usage.
|
|
| 4. |
- Ekblad, Anton, 1986
(författare)
-
A Meta-EDSL for Distributed Web Applications
- 2017
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. ; 52:10, s. 75-85
-
Tidskriftsartikel (refereegranskat)abstract
- We present a domain-specific language for constructing and configuring web applications distributed across any number of networked, heterogeneous systems. Our language is embedded in Haskell, provides a common framework for integrating components written in third-party EDSLs, and enables type-safe, access-controlled communication between nodes, as well as effortless sharing and movement of functionality between application components. We give an implementation of our language and demonstrate its applicability by using it to implement several important components of distributed web applications, including RDBMS integration, load balancing, and fine-grained sandboxing of untrusted third party code. The rising popularity of cloud computing and heterogeneous computer architectures is putting a strain on conventional programming models, which commonly assume that one application executes on one machine, or at best on one out of several identical machines. With our language, we take the first step towards a programming model better suited for a computationally multicultural future.
|
|
| 5. |
- Kovacs, Laura, 1980, et al.
(författare)
-
Coming to terms with quantified reasoning
- 2017
-
Ingår i: ACM SIGPLAN Notices. - New York, NY, USA : ACM. - 1523-2867. ; 52:1, s. 260-270
-
Tidskriftsartikel (refereegranskat)abstract
- The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for functional or imperative programs over inductively defined data types such as lists and trees. However, as the theory of finite term algebras is not finitely axiomatizable, reasoning about quantified properties over term algebras is challenging. In this paper we address full first-order reasoning about properties of programs manipulating term algebras, and describe two approaches for doing so by using first-order theorem proving. Our first method is a conservative extension of the theory of term alge- bras using a finite number of statements, while our second method relies on extending the superposition calculus of first-order theorem provers with additional inference rules. We implemented our work in the first-order theorem prover Vampire and evaluated it on a large number of inductive datatype benchmarks, as well as game theory constraints. Our experimental results show that our methods are able to find proofs for many hard problems previously unsolved by state-of-the-art methods. We also show that Vampire implementing our methods outperforms existing SMT solvers able to deal with inductive data types.
|
|
| 6. |
- Lampropoulos, Leonidas, et al.
(författare)
-
Beginner's luck: a language for property-based generators
- 2017
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. ; 52:1, s. 114-129
-
Konferensbidrag (refereegranskat)abstract
- Property-based random testing a la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these generators can be difficult and error prone. We propose a domain-specific language in which generators are conveniently expressed by decorating predicates with lightweight annotations to control both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. This language, called Luck, makes generators easier to write, read, and maintain. We give Luck a formal semantics and prove several fundamental properties, including the soundness and completeness of random generation with respect to a standard predicate semantics. We evaluate Luck on common examples from the property-based testing literature and on two significant case studies, showing that it can be used in complex domains with comparable bug-finding effectiveness and a significant reduction in testing code size compared to handwritten generators.
|
|
| 7. |
- Sheeran, Mary, 1959
(författare)
-
Functional Programming and Hardware Design: Still Interesting after All These Years
- 2015
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. ; 50:9, s. 165-165
-
Konferensbidrag (refereegranskat)abstract
- Higher order functions provide an elegant way to express algorithms designed for implementation in hardware [1, 6-9]. By showing examples of both classic and new algorithms, I will explain why higher order functions deserve to be studied. Next, I will consider the extent to which ideas from functional programming, and associated formal verification methods, have influenced hardware design in practice [3-5, 10]. What can we learn from looking back? You might ask "Why are methods of hardware design still important to our community?". Maybe we should just give up? One reason for not giving up is that hardware design is really a form of parallel programming. And here there is still a lot to do! Inspired by Blelloch's wonderful invited talk at ICFP 2010 [2], I still believe that functional programming has much to offer in the central question of how to program the parallel machines of today, and, more particularly, of the future. I will briefly present some of the areas where I think that we are poised to make great contributions. But maybe we need to work harder on getting our act together?
|
|
| 8. |
- van der Ploeg, Atze, 1982, et al.
(författare)
-
Practical principled FRP: Forget the past, change the future, FRPNow!
- 2015
-
Ingår i: ACM SIGPLAN Notices. - New York, NY, USA : ACM. - 1523-2867. ; 50:9, s. 302-314
-
Tidskriftsartikel (refereegranskat)abstract
- We present a new interface for practical Functional Reactive Programming (FRP) that (1) is close in spirit to the original FRP ideas, (2) does not have the original space-leak problems, without using arrows or advanced types, and (3) provides a simple and expressive way for performing IO actions from FRP code. We also provide a denotational semantics for this new interface, and a technique (using Kripke logical relations) for reasoning about which FRP functions may "forget their past", i.e. which functions do not have an inherent space-leak. Finally, we show how we have implemented this interface as a Haskell library called FRPNow.
|
|
| 9. |
- Wimmer, M., et al.
(författare)
-
The lock-free k-LSM relaxed priority queue
- 2015
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - New York, NY, USA : ACM. - 0730-8566. ; 50:8, s. 277-278
-
Konferensbidrag (refereegranskat)abstract
- We present a new, concurrent, lock-free priority queue that relaxes the delete-min operation to allow deletion of any of the ρ+1 smallest keys instead of only a minimal one, where ρ is a parameter that can be configured at runtime. It is built from a logarithmic number of sorted arrays, similar to log-structured merge-trees (LSM). For keys added and removed by the same thread the behavior is identical to a non-relaxed priority queue. We compare to state-of-the-art lock-free priority queues with both relaxed and non-relaxed semantics, showing high performance and good scalability of our approach.
|
|
