Feasibility interval for the transactional event handlers of P-FRP

摘要

Functional Reactive Programming (FRP) is a resource aware declarative approach for modeling and building safety-critical embedded systems. Recently, Priority-based FRP (P-FRP) was introduced as a formalism that guarantees real-time response. Due to the state-less nature of execution of functional programs, P-FRP implements a transactional nature of execution where preempted lower-priority tasks are aborted. This makes the response time of a lower-priority task completely dependent on the execution pattern of higher priority tasks. The feasibility interval in the classical preemptive model1 of real-time systems is known and is dependent on the least common multiple (LCM) of task periods. However, since the abort nature of preemption can induce side-effects on the execution of lower-priority tasks, it has been unknown to date if the feasibility in P-FRP is also dependent on the LCM. In this paper, we rigorously prove that these side-effects of preemption are bounded within the LCM and formally derive a value of the feasibility interval in P-FRP. This value of feasibility interval is vital for more robust schedulability analysis of the P-FRP execution model.