Summary of the new research contribution to MegaMart2: A Contract-Based Approach to Scheduling and Verification of Dynamic Dataflow Networks by Jonatan Wiik, Johan Ersfolk and Marina Waldén presented at MEMOCODE’18 (16th ACM-IEEE International Conference on Formal Methods and Models for System Design). Full paper is available here (pdf).
Restricted dataflow models of computation have gained widespread adoption in the safety-critical and real-time domains. As more complex functionality is being incorporated in embedded systems, there is a need for more expressive languages while maintaining high analysability.
In the dataflow programming paradigm, a program is a static network of concurrent actors, which communicate asynchronously through order-preserving channels. Restricted models of computation (MoC), such as Synchronous Dataflow (SDF) [1], have also gained widespread use in the safety-critical and real-time domains because of their high analysability, providing guarantees such as deadlock freedom and boundedness of channels. However, for more complex functionality, restricted MoCs like SDF are often not expressive enough. In the signal processing domain, dynamic dataflow paradigms have gained significant attention, through languages such as the CAL Actor Language [2]. Dynamic dataflow has, however, not gained significant uptake in the safety-critical or real-time domains because scheduling decisions have to be made at runtime. Quasi-static scheduling, e.g. [3], has been proposed as a mean of decreasing the runtime scheduling overhead, by making as many scheduling decisions as possible at compile-time.
In this paper, we present a contract-based approach to scheduling and verification of dynamic dataflow networks. Our approach is based on finding static schedules based on contracts and utilising this information in the verification process. We verify actors and networks to be functionally correct with respect to contracts as well as deadlock free. We build on previous work [4] and show that utilising schedules in the verification process significantly reduces the number of invariant annotations needed. Additionally, we show that the use of contracts can improve runtime performance by allowing scheduling decisions to be made at compile-time.
In a dataflow program, all communication is made explicit through channels, giving actors strong encapsulation with clearly defined interfaces. This also makes contracts a very suitable concept for describing actors and their interaction. In contracts, the developer can state functional properties which the actor or network should adhere to, and make implicit assumptions explicit. Our work is based on two observations: (1) The set of contracts often naturally describe the cyclic behaviour of a dataflow actor or network and can thereby be used to obtain schedules. This means that a contract-based design enables generating more efficient code, as contracts aid the search for schedules. (2) Schedules can make the verification with respect to contracts easier by significantly reducing the number of invariant annotations needed. This is because we can obtain sequential programs from the schedules and verify networks and actors using well-established verification techniques for sequential programs. It has been shown that, given some restrictions on actors, all valid schedules for a dataflow network are functionally equivalent [5]. Hence, we can verify a network for one single schedule, and conclude that the contracts also hold for any valid schedule.
Our scheduling approach is based on state space analysis using the SPIN model checker to find schedules that are optimal with respect to a cost function. As in [4], we use an encoding into the guarded command language Boogie [6] for verification. However, the encoding used here differs from [4] in that it takes into account obtained schedules. Our approach is scalable, as both the scheduling and verification are done hierarchically in a bottom-up manner. It should be noted that it is not always possible to hierarchically schedule networks containing feedback loops. Consequently, it is not possible to schedule every network that would be schedulable non- hierarchically using our approach. However, this can usually be circumvented by flattening one level in the hierarchy.
The main contributions of this paper are the following:
- We show that contracts can aid in the scheduling of dynamic dataflow networks and enables scheduling of actors that do not conform to any well-known statically schedulable model.
- We present a scalable hierarchical scheduling method based on implementation of independent contracts, which can be used to obtain schedules that are optimal with respect to a cost function.
- We present a method to verify that actors and networks are deadlock free and functionally correct with respect to their contracts by utilising schedules.
It is not always possible to schedule networks containing feedback loops hierarchically for a complete repeating period. To solve this, contract level state in combination with finer grained scheduling would be needed. We plan to investigate this as future work. In conclusion, however, our results suggest that contract-based design is useful in dataflow programming at several stages in the development process.
References
- E. A. Lee and D. G. Messerschmitt, “Synchronous data flow,” Proc. IEEE, vol. 75, no. 9, 1987.
- J. Eker. and J. W. Janneck, “CAL language report,” University of California at Berkeley, Tech. Rep. ERL Technical Memo UCB/ERL M03/48, 2003.
- B. Bhattacharya and S. S. Bhattacharyya, “Quasi-static scheduling of reconfigurable dataflow graphs for DSP systems,” in RSP’00, 2000, pp. 84–89.
- J. Wiik and P. Boström, “Specification and automated verification of dynamic dataflow networks,” in SEFM’17, ser. LNCS, vol. 10469. Springer, 2017, pp. 136–151.
- E. A. Lee and T. M. Parks, “Dataflow process networks,” Proc. IEEE, vol. 83, no. 5, 1995.
- M. Barnett, B.-Y. E. Chang, R. Deline, B. Jacobs, and K. R. M. Leino, “Boogie: A modular reusable verifier for object-oriented programs,” in FMCO’05, ser. LNCS. Springer, 2006, vol. 4111.