\n
\n\n \n \n \n \n \n \n Cheap (But Functional) Threads.\n \n \n \n \n\n\n \n Harrison, W. L.; and Procter, A.\n\n\n \n\n\n\n
Higher Order and Symbolic Computation (accepted for publication). 2015.\n
Draft version\n\n
\n\n
\n\n
\n\n \n \n
paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{CheapThreads,\n author = "William L. Harrison and Adam Procter",\n title = "Cheap (But Functional) Threads",\n journal = "Higher Order and Symbolic Computation (accepted for publication)",\n note = {Draft version},\n year = 2015, \n abstract = "This article demonstrates how a powerful and expressive abstraction \nfrom concurrency theory plays a dual role as a programming tool \nfor concurrent applications and as a foundation for their verification.\nThis abstraction---monads of resumptions expressed using monad \ntransformers---is \\emph{cheap}: it is easy to understand, easy to \nimplement, and easy to reason about.\nWe illustrate the expressiveness of the resumption monad with the \nconstruction of an exemplary multitasking operating system kernel \nwith process forking, preemption, message passing, and \nsynchronization constructs in the pure functional programming \nlanguage Haskell.\nBecause resumption computations are stream-like structures, reasoning \nabout this kernel may be posed as reasoning about streams, a problem \nwhich is well-understood. And, as an example, this article \nillustrates how a liveness property---fairness---is proven and \nespecially how the resumption-monadic structure promotes such \nverifications.",\n url_Paper = "https://harrisonwl.github.io/assets/papers/hosc-cheapthreads.pdf",\n}\n\n
\n
\n\n\n
\n This article demonstrates how a powerful and expressive abstraction from concurrency theory plays a dual role as a programming tool for concurrent applications and as a foundation for their verification. This abstraction—monads of resumptions expressed using monad transformers—is \\emphcheap: it is easy to understand, easy to implement, and easy to reason about. We illustrate the expressiveness of the resumption monad with the construction of an exemplary multitasking operating system kernel with process forking, preemption, message passing, and synchronization constructs in the pure functional programming language Haskell. Because resumption computations are stream-like structures, reasoning about this kernel may be posed as reasoning about streams, a problem which is well-understood. And, as an example, this article illustrates how a liveness property—fairness—is proven and especially how the resumption-monadic structure promotes such verifications.\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Provably Correct Development of reconfigurable hardware designs via equational reasoning.\n \n \n \n \n\n\n \n Graves, I.; Procter, A. M.; Harrison, W. L.; and Allwein, G.\n\n\n \n\n\n\n In
Proceedings of the 2015 International Conference on Field-Programmable Technology (FPT '15), pages 160-171, 2015. IEEE\n
\n\n
\n\n
\n\n
\n\n \n \n
paper\n \n \n \n
slides\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{graves15a,\n author = {Graves, Ian and Procter, Adam M. and Harrison, William L. and Allwein, Gerard},\n booktitle = {Proceedings of the 2015 International Conference on\nField-Programmable Technology (FPT '15)},\n isbn = {978-1-4673-9091-0},\n pages = {160-171},\n publisher = {IEEE},\n title = {Provably Correct Development of reconfigurable hardware designs via equational reasoning.},\n year = 2015,\n url_Paper = "https://harrisonwl.github.io/assets/papers/fpt15.pdf",\n url_Slides = "https://harrisonwl.github.io/assets/papers/slides-fpt15.pdf",\n}\n\n
\n
\n\n\n\n
\n
\n\n \n \n \n \n \n \n Semantics Driven Hardware Design, Implementation, and Verification with ReWire.\n \n \n \n \n\n\n \n Procter, A.; Harrison, W. L.; Graves, I.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In
Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM, of
LCTES'15, pages 13:1–13:10, 2015. \n
\n\n
\n\n
\n\n
\n\n \n \n
paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{procter15,\n author = {Procter, Adam and Harrison, William L. and Graves, Ian and Becchi, Michela and Allwein, Gerard},\n title = {Semantics Driven Hardware Design, Implementation, and Verification with ReWire},\n booktitle = {Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM},\n series = {LCTES'15},\n year = {2015},\n isbn = {978-1-4503-3257-6},\n location = {Portland, OR, USA},\n pages = {13:1--13:10},\n articleno = {13},\n numpages = {10},\n abstract = "There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.", \n url_Paper = {https://harrisonwl.github.io/assets/papers/lctes15.pdf},\n} \n\n \n\n
\n
\n\n\n
\n There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation.\n \n \n \n \n\n\n \n Graves, I.; Procter, A.; Harrison, W. L.; Becchi, M.; and Allwein, G.\n\n\n \n\n\n\n In Sano, K.; Soudris, D.; Huebner, M.; and Diniz, P. C., editor(s),
Applied Reconfigurable Computing, volume 9040, of Lecture Notes in Computer Science, pages 41-52. 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n
paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@incollection{graves15,\nyear={2015},\nbooktitle={Applied Reconfigurable Computing},\nvolume={9040},\nseries={Lecture Notes in Computer Science},\neditor={Sano, Kentaro and Soudris, Dimitrios and Huebner, Michael and Diniz, Pedro C.},\ntitle={Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation},\nauthor={Graves, Ian and Procter, Adam and Harrison, William L. and Becchi, Michela and Allwein, Gerard},\npages={41-52},\nabstract = "Although FPGAs have the potential to bring software-like flexibility and agility to the hardware world, designing for FPGAs remains a difficult task divorced from standard software engineering norms. A better programming flow would go far towards realizing the potential of widely deployed, programmable hardware. We propose a general methodology based on domain specific languages embedded in the functional language Haskell to bridge the gap between high level abstractions that support programmer productivity and the need for high performance in FPGA circuit implementations. We illustrate this methodology with a framework for regular expression to hardware compilers, written in Haskell, that supports high programmer productivity while producing circuits whose performance matches and, indeed, exceeds that of a state of the art, hand-optimized VHDL-based tool. For example, after applying a novel optimization pass, throughput increased an average of 28.3 percent over the state of the art tool for one set of benchmarks.",\n url_Paper = "https://harrisonwl.github.io/assets/papers/arc15.pdf",\n}\n\n\n
\n
\n\n\n
\n Although FPGAs have the potential to bring software-like flexibility and agility to the hardware world, designing for FPGAs remains a difficult task divorced from standard software engineering norms. A better programming flow would go far towards realizing the potential of widely deployed, programmable hardware. We propose a general methodology based on domain specific languages embedded in the functional language Haskell to bridge the gap between high level abstractions that support programmer productivity and the need for high performance in FPGA circuit implementations. We illustrate this methodology with a framework for regular expression to hardware compilers, written in Haskell, that supports high programmer productivity while producing circuits whose performance matches and, indeed, exceeds that of a state of the art, hand-optimized VHDL-based tool. For example, after applying a novel optimization pass, throughput increased an average of 28.3 percent over the state of the art tool for one set of benchmarks.\n
\n\n\n