1 Introduction

Nowadays high-assurance systems are often designed as concurrent reactive systems (CRSs) [3]. CRSs react to their computing environment by executing a sequence of commands under an input event. Some examples of CRSs are operating systems (OSs), control systems, and communication systems, which implementation follow an event-driven paradigm. The rely-guarantee technique [16] represents a fundamental approach to compositional reasoning of concurrent programs with shared variables, where programs are represented in imperative languages with extensions for concurrency. Whilst rely-guarantee provides a general framework and can certainly be applied for CRSs, the languages in existing mechanizations of rely-guarantee (e.g. [18, 20, 23, 24, 28]) are imperative and designed only for pure programs, i.e, programs following a flow of procedure calls from an entry point. Examples of reactive systems mentioned above are far more complex than pure programs because they involve many different agents and also heavy interactions with their environment. Without dedicated statements for such system behavior, we often use imperative programs to simulate them, making the formal specification cumbersome, in particular the rely-guarantee conditions. A more detailed motivation will be presented in detail in Sect. 2.

In this paper, we propose PiCore, a two-level event-based rely-guarantee framework for CRSs (Sect. 3). PiCore detaches the specification and the logic of the reactive aspect of systems from event behaviours. Rather than creating yet another framework for modelling and reasoning on events behaviour, PiCore allows to reuse existing rely-guarantee frameworks. The top level introduces the notion of “events” [2, 6] into the rely-guarantee method for system reactions. This level defines the events composing a system, and how and when they are triggered. It specifies the language, semantics, and mechanisms to reason on sequences of events and their execution conditions. The second level focuses on the specification and reasoning of the behaviour of the events composing the first level. PiCore parametrizes the second level using a rely-guarantee interface, allowing to easily reuse existing rely-guarantee frameworks. This design allows PiCore to be independent of the language used to model the behaviour of events.

We have integrated two existing languages and their rely-guarantee proof systems into the PiCore framework. As a result we create two instances of PiCore: and (Sect. 4). integrates the HOL-Hoare_Parallel library in Isabelle/HOL that uses a general imperative language [23]. integrates the CSimpl language in [24]. CSimpl is a generic and realistic imperative language by extending Simpl [25] and providing a rely-guarantee proof system in Isabelle/HOL. Simpl is able to represent a large subset of C99 code and has been applied to the formal verification of seL4 OS kernel [17] at C code level.

We have developed the PiCore framework and its integration with the two languages in Isabelle/HOL, the sources are available at https://lvpgroup.github.io/picore/. As a case study, we have applied PiCore to the formal specification and mechanized proof of the concurrent buddy memory allocation of a real-world OS, Zephyr RTOS [1] (Sect. 5). The formal specification represented in is fine-grained providing a high level of detail. It closely follows the Zephyr C code, covering all the data structures and imperative statements present in the implementation. We use the rely-guarantee proof system in for the formal verification of functional correctness and invariant preservation in the model, revealing three bugs in the C code.

2 Motivation and Approach Overview

Reactive systems respond to continuous stimulus from their computing environment [12] by changing their state and, in turn, affecting their environment by sending back signals to it or initiating other operations. We consider concurrent reactive systems (CRSs), which may involve many different competitive agents executing concurrently with shared resources due to multicore setting, task preemption or embedded interrupts, e.g. concurrent OS kernels [7, 27] and interrupt driven control systems, where the execution of handlers is not atomic. Moreover, the configuration and context of the underlying hardware of systems are not usually encoded in programs, which represent only a portion of the whole system behaviour. For instance, although interrupt handlers (e.g. kernel services and scheduling) in OS kernels are programmed in the C language, when and how interrupts are triggered and which handlers are invoked to react with an interrupt are out of the handler code.

In the setting of imperative languages, CRSs are usually modelled as the parallel composition of reactive systems, each of which is simulated by a while(true) loop program sharing data with its environment and invoking the relevant handlers in the loop body (e.g. [4]). First, The environment non-deterministically decides which event handler is triggered and what are the arguments of the handler for this triggering. Second, some critical properties, such as noninterference of OS kernels [21], concern execution traces of reaction sequences rather than program states only. Without native support in the language semantics, the while loop programs have to use auxiliary logical/program variables to simulate the two non-determinisms together and store the event context of each reactive system. This will make the program and the rely-guarantee conditions unnecessary complicated, in particular for realistic CRSs with many event handlers.

Fig. 1.
figure 1

An example of event

Full size image

The cause of the above problems is the lack of a rely-guarantee approach for system reactions and, as a result, the mixture of system and program behavior together. In this paper, we take the level of abstraction and reusability of the rely-guarantee method a step further by decoupling the two levels using a rely-guarantee interface. The result is a flexible rely-guarantee framework for CRSs, which is able to integrate existing rely-guarantee implementations at program level while being unchanged. At the system reaction level, we consider a reactive system as a set of event handlers called event systems responding to stimulus from the environment. Fig. 1 illustrates an event, which has an event name, a list of input parameters, a guard condition to determine the conditions triggering the event, and an imperative program as its body. In addition to the input parameters, an event has a additional parameter \(\kappa \) which indicates the execution context, e.g. the thread invoking the service and the external devices triggering the interrupt. The execution of an event system concerns the continuous evaluation of guards of the events with their input arguments. From the set of events for which their associated guard condition holds in the current state, one event is non-deterministically selected to be triggered, and its body executed. After the event finishes, the evaluation of guards starts again looking for the next event to be executed. We call the semantics of event systems reactive semantics, where the event context shows the event currently being executed. A CRS is modeled as the parallel composition of event systems that are concurrently executed.

As shown in the Zephyr case study in Sect. 5, the formal specification of CRSs with support for reactions and their composition is much simpler than those represented by pure programs. Furthermore, PiCore supports verifying total correctness of events, whose execution is usually assumed to be terminating, as well as the properties of event systems, whose execution is often non-terminating.

3 PiCore: The Rely-guarantee Framework

This section introduces the event language in PiCore as well as its rely-guarantee proof system, the soundness of proof rules and invariant verification.

3.1 The Event Language

The abstract syntax of PiCore and its semantics are shown in Figs. 2 and 3 respectively. The syntax for events distinguishes basic events pending to be triggered from already triggered events that are under execution. A basic event is defined as \(\mathbf{Event } \ {(l,g,P)}\), where l is the event name, g the guard condition, and \(P\) the body of the event. When \(\mathbf{Event } \ {(l,g,P)}\) is triggered, its body begins to be executed (\(\textsc {BasicEvt}\) rule in Fig. 3) and it becomes a triggered event \(\lfloor {P}\rfloor \). The execution of \(\lfloor {P}\rfloor \) just simulates the program \(P\) (see \(\textsc {TrgdEvt}\) rule in Fig. 3). \(\perp \) is the notation to represent the termination of programs. Instead of defining a language for programs, PiCore reuses existing languages and their rely-guarantee proof systems, which will be discussed in Sect. 4. Events are parametrized in the meta-logic as “\(\lambda (plist, \kappa ). \ \mathbf{Event } \ {(l,g,P)}\)”, where plist is the list of input parameters, and \(\kappa \) is the event system identifier that the event belongs to. These parameters are not part of the syntax of events to make the guard g and the event body P, as well as the rely and guarantee relations, more flexible, allowing to define different instances of the relations for different values of plist and \(\kappa \).

Fig. 2.
figure 2

Abstract syntax of PiCore

Full size image

An event system has two forms that we call event sequence and event set. Event sequences model a sequential execution of events, and event sets model the continuous execution of events from the evaluation of the guards of the events in the set. When the system is not executing any event, one event whose guard condition holds in the current state is non-deterministically chosen to be triggered (\(\textsc {EvtSet}\) rule) and its body P executed (\(\textsc {EvtSeq1}\) rule). After P finishes, the evaluation of the guards starts again looking for the next event to be executed (\(\textsc {EvtSeq2}\) rule). A CRS is modeled by a parallel composition of event systems with shared states. It is a function from \(\mathcal {K}\) to event systems, where \(\mathcal {K}\) indicates the identifiers of event systems. This design is more general and could be applied to track executing events. For instance, we use \(\mathcal {K}\) to represent the core identifier in multicore systems.

The semantics of PiCore is defined via transition rules between configurations. We define a configuration \(\mathcal {C}\) in PiCore as a triple \((\sharp , s, x)\) where \(\sharp \) is a specification, \(s\) is a state, and \(x: \mathcal {K}\rightarrow \mathcal {E}\) is an event context. The event context indicates which event is currently being executed in an event system \(\kappa \). Transition rules in events, event systems, and parallel event systems have the form \(\varSigma \vdash (\sharp _1, s_1, x_1) {\mathop {\longrightarrow }\limits ^{{\delta }}}_{\square } (\sharp _2, s_2, x_2)\), where \(\delta = {t}@{\kappa }\) is a label indicating the type of transition, the subscript “\(\square \)” (\(_e\), \(_{es}\) or \(_{pes}\)) indicates the transition objects, and \(\varSigma \) is used for some static configuration for programs (e.g. an environment for procedure declarations). Here \(t\) indicates a program action c or an occurrence of an event \(\mathcal {E}\). \(@\kappa \) means that the action occurs in event system \(\kappa \). The program transition is denoted as \({\longrightarrow _p}\) in the \(\textsc {TrgdEvt}\) rule. Environment transition rules have the form \(\varSigma \vdash (\sharp , s, x) {\mathop {\longrightarrow }\limits ^{{env}}}_{\square } (\sharp , s', x')\). Intuitively, a transition made by the environment may change the state but not the event context nor the specification. The parallel composition of event systems is fine-grained since small steps in events are interleaved in the semantics of PiCore. This design relaxes the atomicity of events in other approaches (e.g., Event-B [2]).

Fig. 3.
figure 3

Operational semantics of PiCore

Full size image

A computation of PiCore is a sequence of transitions. We define the set of computations of all parallel event systems with static information \(\varSigma \) as \(\varPsi (\varSigma )\), which is a set of lists of configurations inductively defined as follows. The singleton list is always a computation (1). Two consecutive configurations are part of a computation if they are the initial and final configurations of an environment (2) or action transition (3). The operator \(\#\) in \(e\# l\) represents the insertion of element e in list l.

$$ \left\{ \begin{aligned}&(1)[(\mathcal {PS}, s, x)] \in \varPsi (\varSigma ) \\&(2)(\mathcal {PS}, s_1, x_1)\#cs \in \varPsi (\varSigma ) \Longrightarrow (\mathcal {PS}, s_2, x_2)\#(\mathcal {PS}, s_1, x_1)\#cs \in \varPsi (\varSigma ) \\&(3)\varSigma \vdash (\mathcal {PS}_2, s_2, x_2) {\mathop {\longrightarrow }\limits ^{{\delta }}}_{pes} (\mathcal {PS}_1, s_1, x_1) \wedge (\mathcal {PS}_1, s_1, x_1)\#cs \in \varPsi (\varSigma ) \\&\quad \quad \quad \Longrightarrow (\mathcal {PS}_2, s_2, x_2)\#(\mathcal {PS}_1, s_1, x_1)\#cs \in \varPsi (\varSigma ) \end{aligned} \right. $$

Computations for events and event systems are defined in a similar way. We use \(\varPsi (\varSigma ,\mathcal {PS})\) to denote the set of computations of a parallel event system \(\mathcal {PS}\). The function \(\varPsi (\varSigma ,\mathcal {PS}, s, x)\) denotes the computations of \(\mathcal {PS}\) starting up from an initial state \(s\) and event context \(x\).

3.2 Rely-Guarantee Proof System

We consider the verification of two different kinds of properties in the rely-guarantee proof system for reactive systems: pre and post conditions of events and invariants in the fine-grained execution of events. We use the former for the verification of functional correctness of the event, where the pre and post conditions have to be respectively satisfied only before and after the execution of the event. The latter is used on the verification of safety properties concerning the small steps inside events and that must be preserved by any internal step of the event. For instance, in the case of Zephyr RTOS, a safety property is that memory blocks do not overlap each other even during internal steps of the alloc and free services. Other critical properties can also be defined considering the execution trace of events, e.g. noninterference [19, 21, 22].

A rely-guarantee specification in PiCore is a quadruple \(\langle pre, R, G, pst \rangle \), where pre is the precondition, R is the rely condition, G is the guarantee condition, and pst is the post condition. The assumption and commitment functions are denoted by A and C respectively. For each computation \(\varpi \in \varPsi (\varSigma ,\mathcal {E})\), we use \(\varpi _i\) to denote the configuration at index i. \(\sharp _{\varpi _i}\), \(s_{\varpi _i}\), and \(x_{\varpi _i}\) represent the projection of each component in the tuple \(\varpi _i =(\sharp , s, x)\).

figure g

We define validity of rely-guarantee specification for events as

$$ \varSigma \,\models \,{\mathcal {E}} \ \mathbf {sat} \ {\langle pre, R, G, pst \rangle } \equiv \forall s, x. \ \varPsi (\varSigma , \mathcal {E}, s, x) \cap A(\varSigma , pre, R) \subseteq C(\varSigma , G, pst) $$

Intuitively, validity represents that the set of computations cpts starting at the configuration \((\mathcal {E}, s, x)\), with \(s\in pre\) and environment transitions in a computation \(cpt\in cpts\) belonging to the rely relation R, is a subset of the set of computations where action transitions belong to the guarantee relation G and if an event terminates, then the final states belongs to pst. Validity for event systems and parallel event systems are defined in a similar way.

Next, we present the rely-guarantee proof rules in PiCore and their soundness w.r.t validity. The proof rules are shown in Fig. 4, which give us a relational proof method for concurrent systems. We first define \(stable(f,g) \equiv \forall x,y. \ x \in f \wedge (x, y) \in g \longrightarrow y \in f\). Thus, stable(pre, rely) means that the precondition is stable when the rely condition holds. Rules may assume stability of the precondition with regards to the rely relation stable(pre, R) to ensure that the precondition holds after environment transitions.

Fig. 4.
figure 4

Rely-guarantee proof rules for PiCore

Full size image

The \(\textsc {TrgdEvt}\) inference rule says that a triggered event \(\lfloor {P}\rfloor \) satisfies the rely-guarantee specification if the program P satisfies the specification. This rule is directly derived from the semantics for triggered events in Fig. 3, where triggered events modifies the state according to how the program modifies the state. A basic event satisfies its rely-guarantee specification (inference rule \(\textsc {BasicEvnt}\)) if its body satisfies the rely-guarantee strengthening the precondition with the guard of the event. Since the occurrence of an event does not change the state, it is necessary that the guarantee relation includes the identity relation to accept stuttering transitions.

Regarding the proof rules for event systems, sequential composition of events is modeled by \(\textsc {EvtSeq}\) rule, which is similar to that of the sequential command in imperative languages. In order to prove that an event set satisfies its rely-guarantee specification, we have to prove eight premises (\(\textsc {EvtSet}\) rule in Fig. 4). It is necessary that each event together with its specification is derivable in the system (Premise 1). Since the event set behaves as itself after an event finishes, each event postcondition has to imply each event precondition (Premise 2), and the precondition for the event set has to imply the preconditions of all events (Premise 3). An environment transition for the event set corresponds to a transition from the environment of any event i in the event set (Premise 4). The guarantee condition \(Gs_i\) of each event must be in the guarantee condition of the event set, since an action transition of the event set is performed by one of its events (Premise 5). The postcondition of each event must be in the overall postcondition (Premise 6). The last two refer to stability of the precondition and identity of the guarantee relation.

The parallel rule in Fig. 4 establishes compositionality of the proof system, where verification of the parallel specification can be reduced to the verification of individual event systems and then to the verification of individual events. It is necessary that each event system \(\mathcal {PS}(\kappa )\) satisfies its specification \(\langle pres_\kappa , Rs_\kappa , Gs_\kappa , psts_\kappa \rangle \) (Premise 1). The precondition for the parallel composition implies all the event system’s preconditions (Premise 2). An environment transition \(Rs_\kappa \) for the event system \(\kappa \) corresponds to a transition from the overall environment R (Premise 3). Since an action transition of the concurrent system is performed by one of its event system, the guarantee condition \(Gs_\kappa \) of each event system must be a subset of the overall guarantee condition G (Premise 4). The overall postcondition must be a logical consequence of all postconditions of event systems (Premise 5). An action transition of an event system \(\kappa \) should be defined in the rely condition of another event system \(\kappa '\), where \(\kappa \ne \kappa '\) (Premise 6).

Finally, the soundness theorem for a specification \(\sharp \) relates rely-guarantee specifications proven on the proof system with its validity.

Theorem 1

(Soundness). \(\varSigma \vdash {\sharp } \ \mathbf {sat} \ {\langle pre, R, G, pst \rangle } \Longrightarrow \varSigma \,\models \,{\sharp } \ \mathbf {sat} \ {\langle }pre, R, G, pst \rangle \)

3.3 Invariant Verification

In many cases, we would like to show that CRSs preserve certain data invariants. Since CRSs may not be closed systems, i.e. their environment may change the system state that is represented by rely conditions of CRSs, the reachable states of CRSs are dependent on both the initial states and the environment. We define as follows that a CRS \(\mathcal {PS}\) with static information \(\varSigma \), starting up from a set of initial states init under an environment R, preserves an invariant inv when its reachable states satisfy the predicate:

$$ \forall s_0\ x_0\ \varpi .\ \varpi \in \varPsi (\varSigma , \mathcal {PS}, s_0, x_0) \cap A(\varSigma , init, R) \longrightarrow (\forall i<len(\varpi ).\ inv(s_{\varpi _i})) $$

In this definition, \(\varpi \) denotes an arbitrary computation of \(\mathcal {PS}\) from a set of initial states init and under an environment R. It requires that all states in \(\varpi \) satisfy the invariant inv. \(\{s \mid P(s)\}\) denotes the set of states s satisfying P.

To show that inv is preserved by a system \(\mathcal {PS}\), it suffices to show the invariant verification theorem as follows. This theorem indicates that (1) the system satisfies its rely-guarantee specification \(\langle init, R, G, post \rangle \), (2) inv initially holds in the set of initial states, and (3) each action transition as well as each environment transition preserve inv. Later, by the proof system of PiCore, invariant verification is decomposed to the verification of individual events.

Theorem 2

(Invariant Verification). For formal specification \(\mathcal {PS}\) and \(\varSigma \), a state set init, a rely condition R, and inv, if

  • \(\varSigma \vdash {\mathcal {PS}} \ \mathbf {sat} \ {\langle init, R, G, post \rangle }\).

  • \(init \subseteq \{s \mid inv(s)\}\).

  • \(stable(\{s \mid inv(s)\}, R)\) and \(stable(\{s \mid inv(s)\}, G)\) are satisfied.

then inv is preserved by \(\mathcal {PS}\) w.r.t. init and R.

4 Integrating Concrete Languages

We present the rely-guarantee interface of PiCore framework in this section as well as the integration of the IMP and CSimpl languages.

4.1 Rely-Guarantee Interface of PiCore Framework

To implement a flexible integration of languages for programs on event bodies, PiCore provides a rely-guarantee interface that program languages must respect. The interface is an abstraction for common rely-guarantee components required by PiCore (Fig. 5). These components are represented as a set of parameters and assumptions to guarantee the correctness of the proof system, since the language, semantics, proof rules and soundness proof of PiCore in Sect. 3 are developed using this interface.

Following this interface, third-party languages and their rely-guarantee proof systems are embedded into PiCore as interpretations using an adapter that implements the interface. Since these languages may have existed for years, they are not necessary completely consistent with the PiCore interface. Hence, for each language that we want to integrate in PiCore it is necessary to provide a rely-guarantee adapter to bridge the differences of rely-guarantee components between PiCore and the languages. The adapter implements the interface by delegating functionality of the event language to the integrated language. This architecture makes it possible to integrate existing languages without modifying their specification, semantics, and rely-guarantee inference system.

Fig. 5.
figure 5

PiCore framework and its integration with imperative languages

Full size image

The interface requires specifications and assumptions for four differentiated elements: language definition (syntax and semantics), rely-guarantee definitions (computation and rely-guarantee validity), rely-guarantee proof rules, and their soundness.

As a parametric framework, PiCore does not define the syntax for languages of programs. It only requires a notation to represent the termination of programs, which is denoted as \(\perp \) in PiCore (Parameter 1 in Table 1). PiCore also needs the transition relations representing the event behaviour (event action) and the environment (Parameters 2 and 3). To reason about event behaviors, PiCore assumes that (1) program \(\perp \) cannot take a step to another state (Assumption 1 in Table 2), (2) if a program P takes an action transition, the program is changed in the next configuration (Assumption 2), and (3) environment transitions do not change the program itself (Assumption 3).

Since the body of events in PiCore is specified using external languages, computations and the reasoning of events are dependent on those languages. PiCore requires the specification for computation of programs (Parameters 4 and 5) and assumes that (1) a computation of any program is not empty (Assumption 4), (2) if \(\varpi \) is a computation of a language and the program of its first configuration is P, then \(\varpi \) is a computation for the program P (Assumption 5), and (3) there are three constructions for computation of programs (Assumption 6), which is similar to the definition of events we have presented in Sect. 3.

Finally, the interface requires the components related to the validity of rely-guarantee specification and the proof rules (Parameters 6–9). The definitions of the assume/commit functions and validity are similar to those in PiCore (see Sect. 3), and are relaxed to be not necessarily equivalent. PiCore requires that the rely-guarantee proof rules in languages are sound (Assumption 10). Other rely-guarantee components, such as rely and guarantee condition, are defined in the above parameters at the same time.

Table 1. Parameters of PiCore
Full size table
Table 2. Assumptions of parameters
Full size table

4.2 Integrating the IMP and CSimpl languages

To integrate a language and its rely-guarantee framework into PiCore, we first create an adapter for the language providing the PiCore interface. For each parameter in the interface, there is a corresponding definition (or function) in the adapter instantiating the parameter. Moreover, the adapter provides the necessary set of lemmas and theorems to show that the instances of the interface specifications satisfy the interface assumptions.

In the mechanized implementation of PiCore in Isabelle/HOL, we use locales to create the framework, where parameters and assumptions of PiCore are represented as parameters and assumptions of locales. Locales are the Isabelle’s approach for dealing with parametric theories. Using locale interpretations, they may be instantiated by assigning concrete data to parameters, and conclusions of locales will be propagated to the current theory or the current proof context. Using the notion of locales, we create PiCore instances by interpreting the PiCore locale using adapters for IMP and CSimpl.

Since the definitions of rely-guarantee components in IMP [23] are consistent with the PiCore interface, except that there is no static information \(\varSigma \) in IMP, the adapter for IMP is straightforward from its rely-guarantee specification, we omit the details here and the interested reader can refer to the Isabelle/HOL sources.

More interesting is CSimpl that supports most of the features of real world programming languages including exceptions, and is substantially more complex than IMP. Here, we show the adapter for CSimpl. The language and its rely-guarantee proof system are presented in detail in [24]. The abstract syntax of CSimpl is defined as in Fig. 6 in terms of states, of type ’s; a set of fault types, of type ’f; a set of procedure names of type ’p, and a set of simulation events ’e (simulation events are not addressed in this work). Type (’s,’p,’f,’e) config defines the configuration used in its transition semantics and (’s,’p,’f,’e) body denoted as \(\varGamma \) defines the procedure declarations as mapping from procedure names to CSimpl programs. (’s,’p,’f,’e) confs defines the type of computations. To support reasoning about procedure invocations, CSimpl uses the notation \(\varTheta \) to maintain the rely-guarantee specification for procedures. The validity in CSimpl requires that each procedure satisfies its specification.

Fig. 6.
figure 6

Syntax and state definition of the CSimpl Language [24]

Full size image

In the adapter, we first use the pair \((\varGamma ,\varTheta )\) to instantiate the environment \(\varSigma \) in PiCore. We instantiate the termination statement as the Skip command in CSimpl. The program transition in CSimpl is \(\varGamma \vdash _c (P,s) \longrightarrow (Q,t)\), and it is adapted as \((\varGamma ,\varTheta ) \vdash _{cI} (P,s) \longrightarrow (Q,t) \equiv \varGamma \vdash _c (P,s) \longrightarrow (Q,t)\). CSimpl semantics for programs can transit from a Normal state to a different type. However, it does not allow transitions from a non Normal state to any other state. Therefore, the environment transition in CSimpl is defined as follows.

$$ \left\{ \begin{aligned}&\varGamma \vdash _c (P,Normal\ s) \longrightarrow _{env} (P,t) \\&(\forall t'.\ t \ne Normal\ t') \Longrightarrow \varGamma \vdash _c (P,t) \longrightarrow _{env} (P,t) \end{aligned} \right. $$

To adapt the restricted environment transition, we first define the environment transition in the adapter as \((\varGamma ,\varTheta ) \vdash _{cI} (P, s) \longrightarrow _{env} (P,t)\), which allows any state transition and is compatible with that in the interface. Then, we restrict the rely condition in the definition of proof rules in the adapter to bridge this difference, which will be discussed later. Based on the transition functions, the computation function \(\varPsi \) of the adapter is defined in the same form as in CSimpl.

The rely-guarantee specification in CSimpl is in the form [p, R, G, (q, a)], where the postcondition (q, a) is a pair of state sets. The set q constrains the final state if the program terminates as Skip representing a normal state, whilst a constrains abrupt terminations in an exception with the command Throw. The assume and commit functions in CSimpl are like PiCore, but considering the fault states and abrupt termination. The validity function of CSimpl is defined in the same form as in PiCore. For procedure invocations, CSimpl defines another validity function using the general one, which also requires that each procedure satisfies its rely-guarantee specification.

We define the assume, commit and validity functions in the adapter as the same form as in PiCore. In CSimpl preconditions are over normal states. For type consistency PiCore does not impose that restriction, but rather it is enforced by the adapter to bridge the difference, which will be discussed later. PiCore does restrict the final statement to Skip thus exceptions have to be handled at program level. This restriction is motivated by the second assumption in the rule \(\textsc {EvtSet}\) for PiCore proof system in Fig. 4, since postconditions of events must imply their preconditions, and preconditions in CSimpl are sets of normal states, a final configuration of an event cannot throw an exception.

Finally, based on the definition of the proof rules in CSimpl, we define proof rules in the adapter as follows. (1) The validity in CSimpl only concerns preconditions of Normal states, so we restrict the precondition p to Normal. (2) Programs of an event body cannot throw exceptions to the event level, so final states when reaching the final statement Skip are Normal. Thus, we restrict the postcondition q to Normal. (3) Events assume the normal execution of their program body, and furthermore the program cannot fall into a Fault state. So we assume the Fault set F to be empty. In addition, the program P should satisfy its rely-guarantee specification in CSimpl. (4) The environment transition in CSimpl does not allow transitions from a non Normal state to a different state, we represent it in the rely condition R. (5) Finally, the rely-guarantee specification for each procedure in \(\varTheta \) has to be satisfied.

figure i

To interpret the PiCore framework using the adapter, we have to show that the assumptions in Table 2 are preserved on the adapted definitions. The preservation of assumptions 1–9 are straightforward. To show assumption 10, we prove that

figure j

5 Concurrent Memory Management of Zephyr RTOS

In this section, we use , the instantiation of PiCore with IMP, to formally specify and verify the concurrent memory management of Zephyr RTOS (for more detail refer to [29]). During the formal verification, we found 3 bugs in the C code of Zephyr: an incorrect block split, an incorrect return, and non-termination of a loop in the k_mem_pool_alloc service. The first two bugs are critical and have been repaired in the latest release of Zephyr.

The buddy memory allocation can split large blocks into smaller ones to fit as best as possible the requested size. This allows blocks of different sizes to be allocated and released efficiently while limiting memory fragmentation concerns. The memory is organized by levels, each “level n” block is a quad-block that can be split into four smaller “level (n+1)” blocks of equal size. This process is repeated until blocks reach a minimum level for which splitting is not possible. In our formal specification, we define the structure of a memory pool as illustrated in Fig. 7. The top of the figure shows the real memory of the first block at level 0.

Fig. 7.
figure 7

Structure of memory pools

Full size image

Thread preemption and fine-grained locking make kernel execution of memory services concurrent. Zephyr provides two kernel services k_mem_pool_alloc and k_mem_pool_free, for memory allocation and release respectively. When an application requests a memory block, Zephyr first computes a value \(free\_l\) that is the lowest level containing free memory blocks. Due to concurrency, when a service tries to allocate a free block blk from level \(free\_l\), blocks at that level may be allocated or merged into a bigger block by other concurrent threads. In such a case the service will back out to retry. Allocation supports a timeout parameter to allow threads waiting for that pool for a period of time when the call does not succeed. If the allocation fails and the timeout is not K_NO_WAIT, the thread is suspended and the context is switched to another thread.

We define a rich set of invariants on the kernel state clarifying the constraints and consistency of quad trees, free block lists, memory pool configuration, and waiting threads. From the well-shaped properties of quad trees, we derive a critical property to prevent memory leaks: memory blocks cover the whole memory address of the pool, but do not overlap each other. Memory blocks of a memory pool mp are a partition of the pool where for any memory address addr in the address space of a memory pool, i.e. \(addr < n\_max * max\_sz\), there is one and only one memory block whose address space contains addr. The predicate is defined as follows.

figure l

From the invariants of the well-shaped bitmap, we derive the general property for the memory partition.

Theorem 3

(Memory Partition). For any kernel state s, If the memory pools in s are consistent in their configuration, and their bitmaps are well-shaped, the memory pools satisfy the partition property in s:

In the formal specification, we consider a scheduler \(\mathcal {S}\) and a set of threads \(t_1, ..., t_n\). Each user thread \(t_i\) invokes allocation and release services, thus the event system for \(t_i\) is

figure m

which is a set of alloc and free events, where the input parameters for these events correspond with the arguments of the service implementation in the C code. Events are parametrized by a thread identifier \(t_i\) used to control access to the execution context of the thread invoking it. Together with the threads we model the event service for the scheduler \(esys_{sched}\) consisting of a unique event sched whose argument is a thread t to be scheduled when it is in the READY state. The formal specification of the memory management is thus defined as: . This is much simpler than the specification obtained from a non-event oriented language.

Using the compositional reasoning of , correctness of Zephyr memory management can be specified and verified with the rely-guarantee specification of each event. The functional correctness of a kernel service is specified by its pre/post conditions. The preservation of invariants, memory configuration, and separation of local variables is specified in the guarantee condition of each service. Although IMP does not have proof rules for loop termination, we use a logical variable \(\alpha \) to parametrize the loop invariants and prove the termination of loop statements in Zephyr by finding a convergent relation to show that the number of iterations is finite.

The guarantee condition for both memory services is defined as:

figure p

This relation states that a step from alloc or free may not change the state (1), e.g., selecting a branch on a conditional statement. If it changes the state then: (2) static configuration of memory pools in the model does not change; (3.1) if the scheduled thread is not the thread invoking the event then its local variables do not change; (3.2) if it is, then the relation preserves the memory invariant; (4) a thread does not change the local variables of other threads.

Using PiCore and IMP proof rules we verify that the invariant is preserved by all the events. Additionally, we prove that when starting in a valid memory configuration given by the invariant, and if the service does not return an error code, then it returns a valid memory block with size bigger or equal to the requested capacity.

6 Evaluation and Conclusion

Evaluation. We use Isabelle/HOL as the specification and verification system. All derivations of our proofs have passed through the Isabelle proof kernel. We use \(\approx \)9,200 lines of specification and proof (LOSP) to develop the PiCore framework. The IMP language and its rely-guarantee proof system consist of \(\approx \)2,400 LOSP, and CSimpl \(\approx \)15,000 LOSP. The two parts of specification and proof are completely reused in and respectively. The adapter of IMP is \(\approx \)650 LOSP including new proof rules and their soundness as well as a concrete syntax. The adapter of CSimpl is \(\approx \)400 LOSP. Finally, we develop \(\approx \)17,600 LOSP for the Zephyr case study, 40 times more than the lines of the C code due to the in-kernel concurrency, where invariant proofs represent the largest part.

Related Works. The rely-guarantee approach has been mechanized in Isabelle/HOL (e.g. [13, 14, 23, 24, 26]) and Coq (e.g. [18, 20]). In [13, 14], an abstract algebra of atomic steps is developed, and rely/guarantee concurrency is an interpretation of the algebra. To allow a meaningful comparison of rely-guarantee semantic models, two abstract models for rely-guarantee are developed and mechanized in [26]. None of both work consider any concrete imperative languages for rely-guarantee. The works [20, 23] mechanize the rely-guarantee approach for simple imperative languages. Later, a rely-guarantee proof system is developed in Isabelle/HOL for CSimpl [24], a generic and realistic concurrent imperative language by extending the sequential language Simpl [25]. These mechanizations focus on imperative languages for pure programs, of which two of them [23, 24] have been integrated in PiCore.

Refinement of reactive systems [5] and the subsequent Event-B approach [2] propose a refinement-based formal method for system-level modeling and analysis. In [15], an Event-B model is created to mimic rely-guarantee style reasoning for concurrent programs, but not to provide a rely-guarantee framework for Event-B. The rely-guarantee reasoning for event-based applications has been studied in [8,9,10,11]. The definition of events is similar to PiCore. They extend a simple, sequential, imperative language by primitives for announcing and consuming events, announce(e) and consume(e(x)) where e is an event. Therefore, events are triggered by imperative programs in another event. This is very different from the reactive semantics in PiCore where the system is non-deterministically executed simulating a real reactive system. Moreover, the language to specify events in these works is a simple imperative language, whilst PiCore has an open interface for the integration and reusability of different languages and frameworks.

Conclusion and Future Work. In this paper, we propose an event-based rely-guarantee framework for concurrent reactive systems. This approach is open to the specification of event behaviours. It provides an interface to integrate systems for specification and reasoning at that level that eases formal methods reusability. We have mechanized the integration of the IMP and CSimpl languages and their proof systems into PiCore in the Isabelle/HOL theorem prover. We show the simplicity of events to represent concurrent reactive systems and the usefulness of PiCore for realistic systems in the verification of the concurrent buddy memory allocation of Zephyr RTOS. As future work, we plan to extend PiCore to support more event structures and step-wise refinement.