Ivan Perez
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and Functional Reactive Programming capture the essence of those languages in a way that is both elegant and robust.
To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many Functional Reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults, and incorporating fault tolerance into Functional Reactive Programming, requires a different construction and remains an open problem.
This work presents extensions to an existing functional reactive abstraction to facilitate tagging reactive transformations with hazard tags or confidence levels. We present a prototype framework to quantify the reliability of a reactive construction, by means of numeric factors or probability distributions, and demonstrate how to aid the design of fault-tolerant systems, by constraining the allowed reliability to required boundaries. By applying type-level programming, we show that it is possible to improve static analysis and have compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide their analysis and design, to test system properties, to verify fault tolerance properties, to perform runtime monitoring, to implement fault tolerance during execution and to address faults during runtime. We present implementations in Haskell and in Idris.
Supplemental Material
- 1992. DO-178B: Software Considerations in Airborne Systems and Equipment Certification. (1992).Google Scholar
- Algirdas Avižienis. 1967. Design of Fault-tolerant Computers. In Proceedings of the November 14-16, 1967, Fall Joint Computer Conference (AFIPS ’67 (Fall)). ACM, New York, NY, USA, 733–743.Google ScholarDigital Library
- Algirdas Avižienis. 1976. Fault-tolerant systems. IEEE Trans. Computers 25, 12 (1976), 1304–1312. Google ScholarDigital Library
- Manuel Bärenz and Ivan Perez. 2018. Rhine - FRP with type-level clocks. In Haskell Symposium. (Submitted).Google ScholarDigital Library
- Manuel Bärenz, Ivan Perez, and Henrik Nilsson. 2016. Mathematical Properties of Monadic Stream Functions. http: //cs.nott.ac.uk/~ixp/papers/msfmathprops.pdf . (2016).Google Scholar
- Gérard Berry, Amar Bouali, Xavier Fornari, Emmanuel Ledinot, Eric Nassor, and Robert De Simone. 2000. Esterel: A formal method applied to avionic software development. Science of Computer Programming 36, 1 (2000), 5–25. Google ScholarDigital Library
- Frédéric Boussinot and Robert De Simone. 1991. The ESTEREL language. Proc. IEEE 79, 9 (1991), 1293–1304.Google ScholarCross Ref
- Jan Bracker and Henrik Nilsson. 2015. Polymonad Programming in Haskell. In Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages (IFL ’15). ACM, New York, NY, USA, Article 3, 12 pages. Google ScholarDigital Library
- Jan Bracker and Henrik Nilsson. 2016. Supermonads: One Notion to Bind Them All. In Proceedings of the 9th International Symposium on Haskell (Haskell 2016). ACM, New York, NY, USA, 158–169. Google ScholarDigital Library
- Edwin Brady. 2013. Programming and reasoning with algebraic effects and dependent types. In ACM SIGPLAN Notices, Vol. 48. ACM, 133–144. Google ScholarDigital Library
- Ricky W. Butler. 2008. A Primer on Architectural Level Fault Tolerance. Technical Report NASA/TM-2008-215108, L-19403. NASA Langley Research Center.Google Scholar
- Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM, New York, NY, USA, 268–279. Google ScholarDigital Library
- Antony Courtney, Henrik Nilsson, and John Peterson. 2003. The Yampa arcade. In Haskell Workshop. 7–18. Google ScholarDigital Library
- Judith Crow and Ben Di Vito. 1998. Formalizing Space Shuttle software requirements: Four case studies. ACM Transactions on Software Engineering and Methodology (TOSEM) 7, 3 (1998), 296–332. Google ScholarDigital Library
- Ben L Di Vito. 1996. Formalizing new navigation requirements for NASA’s space shuttle. In International Symposium of Formal Methods Europe. Springer, 160–178. Google ScholarDigital Library
- Ben L Di Vito. 1999. A model of cooperative noninterference for integrated modular avionics. In Dependable Computing for Critical Applications 7, 1999. IEEE, 269–286. Google ScholarDigital Library
- Ben L DiVito and Larry W Roberts. 1996. Using formal methods to assist in the requirements analysis of the space shuttle GPS change request. (1996).Google Scholar
- Francois-Xavier Dormoy. 2008. Scade 6: a model based solution for safety critical software development. In Proceedings of the 4th European Congress on Embedded Real Time Software (ERTSâĂŹ08). 1–9.Google Scholar
- Bruno Dutertre and Victoria Stavridou. 1997. Formal requirements analysis of an avionics control system. IEEE Transactions on Software Engineering 23, 5 (1997), 267–278. Google ScholarDigital Library
- Conal Elliott and Paul Hudak. 1997. Functional Reactive Animation. In ACM SIGPLAN Notices, Vol. 32(8). 263–273. Google ScholarDigital Library
- Jeff Epstein, Andrew P Black, and Simon Peyton-Jones. 2011. Towards Haskell in the cloud. In ACM SIGPLAN Notices, Vol. 46. ACM, 118–129. Google ScholarDigital Library
- Martin Erwig and Steve Kollmansberger. 2006. Functional pearls: Probabilistic functional programming in Haskell. Journal of Functional Programming 16, 1 (2006), 21–34. Google ScholarDigital Library
- Nicholas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9 (1991), 1305–1320.Google Scholar
- Frank Huch and Ulrich Norbisrath. 2000. Distributed programming in Haskell with ports. In Symposium on Implementation and Application of Functional Languages. Springer, 107–121. Google ScholarDigital Library
- John Hughes. 2000. Generalising monads to arrows. Science of Computer Programming 37, 1 (2000), 67 – 111. Google ScholarDigital Library
- Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. ACM SIGPLAN Notices 49, 1 (2014), 633–645. Google ScholarDigital Library
- Oleg Kiselyov, Amr Sabry, and Cameron Swords. 2013. Extensible effects: an alternative to monad transformers. In ACM SIGPLAN Notices, Vol. 48. ACM, 59–70. Google ScholarDigital Library
- Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS) 32, 1 (2014), 2. Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM, 207–220. Google ScholarDigital Library
- Sheng Liang, Paul Hudak, and Mark Jones. 1995a. Monad transformers and modular interpreters. In Symposium on Principles of programming languages. 333–343. Google ScholarDigital Library
- Sheng Liang, Paul Hudak, and Mark Jones. 1995b. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 333–343. Google ScholarDigital Library
- Patrick Lincoln and John Rushby. {n. d.}. Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model. In Computer Assurance, 1994. COMPASS’94 Safety, Reliability, Fault Tolerance, Concurrency and Real Time, Security. Proceedings of the Ninth Annual Conference on. IEEE, 107–120.Google Scholar
- Patrick Lincoln and John Rushby. 1993. A formally verified algorithm for interactive consistency under a hybrid fault model. In Fault-Tolerant Computing, 1993. FTCS-23. Digest of Papers., The Twenty-Third International Symposium on. IEEE, 402–411. Google ScholarDigital Library
- Patrick Maier, Robert Stewart, and Phil Trinder. 2014. The HdpH DSLs for Scalable Reliable Computation. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). ACM, New York, NY, USA, 65–76. Google ScholarDigital Library
- Henrik Nilsson, Antony Courtney, and John Peterson. 2002. Functional reactive programming, continued. In Haskell Workshop. 51–64. Google ScholarDigital Library
- Dominic Orchard and Tomas Petricek. 2014. Embedding Effect Systems in Haskell. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). ACM, New York, NY, USA, 13–24. Google ScholarDigital Library
- Dominic Orchard and Tomas Petricek. 2015. Embedding effect systems in Haskell. ACM SIGPLAN Notices 49, 12 (2015), 13–24. Google ScholarDigital Library
- Dominic A. Orchard, Tomas Petricek, and Alan Mycroft. 2014. The semantic marriage of monads and effects. CoRR abs/1401.5391 (2014). arXiv: 1401.5391 http://arxiv.org/abs/1401.5391Google Scholar
- Sam Owre, Sreeranga Rajan, John M Rushby, Natarajan Shankar, and Mandayam Srivas. 1996. PVS: Combining specification, proof checking, and model checking. In International Conference on Computer Aided Verification. Springer, 411–414. Google ScholarDigital Library
- S. Owre, J. M. Rushby, , and N. Shankar. 1992. PVS: A Prototype Verification System. In 11th International Conference on Automated Deduction (CADE) (Lecture Notes in Artificial Intelligence), Deepak Kapur (Ed.), Vol. 607. Springer-Verlag, Saratoga, NY, 748–752. http://www.csl.sri.com/papers/cade92-pvs/ Google ScholarDigital Library
- Sam Owre, Natarajan Shankar, John M Rushby, and David WJ Stringer-Calvert. {n. d.}. PVS language reference. ({n. d.}).Google Scholar
- Bruno Pagano, Olivier Andrieu, Thomas Moniot, Benjamin Canou, Emmanuel Chailloux, Philippe Wang, Pascal Manoury, and Jean-Louis Colaço. 2009. Experience Report: Using Objective Caml to Develop Safety-critical Embedded Tools in a Certification Framework. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09). ACM, New York, NY, USA, 215–220. Google ScholarDigital Library
- Ivan Perez. 2017. Back to the Future: Time Travel in FRP. In Proceedings of the 10th ACM SIGPLAN International Haskell Symposium (Haskell 2017). ACM, New York, NY, USA, 12. Google ScholarDigital Library
- Ivan Perez, Manuel Bärenz, and Henrik Nilsson. 2016. Functional Reactive Programming, Refactored. In Proceedings of the 9th International Symposium on Haskell (Haskell 2016). ACM, New York, NY, USA, 33–44. Google ScholarDigital Library
- Ivan Perez and Henrik Nilsson. 2017. Testing and Debugging Functional Reactive Programming. Proc. ACM Program. Lang. 1, ICFP, Article 2 (Aug. 2017), 27 pages. Google ScholarDigital Library
- Holger Pfeifer, Detlef Schwier, and Friedrich W Von Henke. 1999. Formal verification for time-triggered clock synchronization. In Dependable Computing for Critical Applications 7, 1999. IEEE, 207–226. Google ScholarDigital Library
- Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. 2010. Copilot: a hard real-time runtime monitor. In International Conference on Runtime Verification. Springer, 345–359. Google ScholarDigital Library
- Lee Pike, Sebastian Niller, and Nis Wegmann. 2012. Runtime Verification for Ultra-Critical Systems. In Runtime Verification, Sarfraz Khurshid and Koushik Sen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 310–324. Google ScholarDigital Library
- John Rushby. {n. d.}. PVS Bibliography. http://pvs.csl.sri.com/documentation.shtml . ({n. d.}).Google Scholar
- Butler RW. 1996. An introduction to requirements capture using PVS: Specification of a simple autopilot. (1996).Google Scholar
- Mike Spivey. 1990. A functional theory of exceptions. Science of computer programming 14, 1 (1990), 25–42. Google ScholarDigital Library
- Robert Stewart. 2013. Reliable massively parallel symbolic computing: fault tolerance for a distributed Haskell. Ph.D. Dissertation. Heriot-Watt University.Google Scholar
- Robert Stewart, Patrick Maier, and Phil Trinder. 2016. Transparent fault tolerance for scalable functional computation. Journal of Functional Programming 26 (2016).Google Scholar
- Robert Stewart, Phil Trinder, and Patrick Maier. 2013. Supervised Workpools for Reliable Massively Parallel Computing. In Trends in Functional Programming, Hans-Wolfgang Loidl and Ricardo Peña (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 247–262. Google ScholarDigital Library
- Phil Trinder, Robert Pointon, and Hans-Wolfgang Loidl. 2000. Towards Runtime System Level Fault Tolerance for a Distributed Functional Language. Trends in Functional Programming 2 (2000), 103.Google Scholar
- Steve Vinoski. 2007. Reliability with Erlang. IEEE Internet Computing 11, 6 (2007). Google ScholarDigital Library
- Philip Wadler. 1985. How to replace failure by a list of successes. In Conference on Functional Programming Languages and Computer Architecture. Springer, 113–128. Google ScholarDigital Library
- David Walker, Lester Mackey, Jay Ligatti, George A. Reis, and David I. August. 2006. Static Typing for a Faulty Lambda Calculus. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). ACM, New York, NY, USA, 38–49. Google ScholarDigital Library
- Libin Xu, Yuebin Bai, Kun Cheng, Lingyu Ge, Danning Nie, Lijun Zhang, and Wenjia Liu. 2016. Towards Fault-Tolerant RealTime Scheduling in the seL4 Microkernel. In High Performance Computing and Communications; IEEE 14th International Conference on Smart City; IEEE 2nd International Conference on Data Science and Systems (HPCC/SmartCity/DSS), 2016 IEEE 18th International Conference on. IEEE, 711–718.Google Scholar
Index Terms
- Fault tolerant functional reactive programming (functional pearl)
Recommendations
Functional reactive programming, refactored
Haskell 2016: Proceedings of the 9th International Symposium on HaskellFunctional Reactive Programming (FRP) has come to mean many things. Yet, scratch the surface of the multitude of realisations, and there is great commonality between them. This paper investigates this commonality, turning it into a mathematically ...
Functional reactive programming, refactored
Haskell '16Functional Reactive Programming (FRP) has come to mean many things. Yet, scratch the surface of the multitude of realisations, and there is great commonality between them. This paper investigates this commonality, turning it into a mathematically ...
Functional reactive programming, continued
Haskell '02: Proceedings of the 2002 ACM SIGPLAN workshop on HaskellFunctional Reactive Programming (FRP) extends a host programming language with a notion of time flow. Arrowized FRP (AFRP) is a version of FRP embedded in Haskell based on the arrow combinators. AFRP is a powerful synchronous dataflow programming ...
Comments