Jean-Pierre Talpin
email: talpin@irisa.fr

Paul Le Guernic

Sandeep Kumar Shukla
email: shukla@vt.edu

Rajesh K Gupta
email: rgupta@ucsd.edu

Sandeep Kumar

A compositional behavioral

Keywords: Embedded system design, formal methods, models of computation, program transformation, verification

INTRODUCTION

The popular slogan "write once, run anywhere" effectively renders the expressive capabilities of general purpose programming languages for developing, deploying, and reusing target-independent applications. Generality and simplicity has driven most attention of the compiler technology community to developing local and compositional compiler optimization techniques. When it comes to the implementation of embedded software, this approach is however far from satisfactory, especially in hard real-time system design (e.g. airborne systems, digital circuits) where conformance to real-time specifications is critical.

Domain-specific models and languages, such as these proposed under the synchronous programming paradigm, provides the necessary formal engineering models and design methodologies to allow for a program written once to be mapped on any distributed execution architecture by using global transformation and optimization techniques. Our aim is to relate this domain-specific model to embedded software development using generalpurpose environments. To this end, we set the methodological framework of our synchronous model of computation within the general and reusable concept of a type system targeting the generic programming language setting of GCC's intermediate representations (three-address code and static single assignment). We give formal semantics to both our type system and the functional subset of SSA under consideration, define a type inference system and prove its correctness, before to depict the applications of our technique as developed in our project and presented in previous works.

A functional application domain. We consider embedded software implemented by resource-constrained [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF] multi-threaded programs on a specific runtime sub-system (e.g. , the real-time JVM, an RTOS, or simply hardware) which we call its execution architecture. Our technique consists of a type inference system that relates threads (imperative programs in intermediate form) to propositions expressed by synchronous transition systems that describe their behaviour. Example. On the right, we outline the extent of our technique by depicting a test-case studied in [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF] . We consider modeling a real-time Java program consisting of three threads (right), a scheduler (top-left) and shared resources control (bottom-left). This decomposition is obtained by partitioning the executable program and its environment into:

-the execution architecture: a hardware platform, a middle-ware library, a real-time operating system, a virtual machine (e.g. in Java), a simula- [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF] It is common sense to restrict ourselves to programs where all objects are first created and initialized to elaborate the application architecture. Then, threads implement reactions to inputs in the nominal phase of execution and do not allocate any new object (to comply with certification requirement in software design or simply with common sense in SoC design).

tion kernel (e.g. in SystemC). The execution architecture describes an API of generic process and communication management services.

-the application architecture: a program, starting from the main() procedure, which initializes and links objects to form a hierarchical structure of shared data and communicating threads. The application mapping constructively describes the architecture of the system.

-the application functionalities: a set of program threads which periodically or sporadically react to inputs from the environment by interacting with each other for the access to shared data.

Our methodology consists of considering the three elements of an embedded system (its execution and application architectures, its application functionalities) in specific ways.

-modeling: the execution architecture, viewed through an application programming interface (API) of generic services, is modeled by template propositions. For instance, the procedure for thread creation in an RTOS API corresponds to a template proposition in the RTOS model whose parameters are the number of threads supported by the application scheduler, the period and deadline of the thread (for a real-time thread), etc.

-analysis: the application architecture, viewed as a hierarchical structure, is interpreted to elaborate a model by the instantiation of generic API services to the parameters and initial values provided in the program (e.g. thread parameters).

-translation: each thread consists of a sequential program that describes a functionality to be periodically or sporadically executed by the scheduler and corresponds to a particular model.

This allows for a complete separation of the virtual (threading or functional) architecture of an application from its actual, real-time and resourceconstrained implementation: it provides an implementation of the "write once run anywhere" slogan in embedded system design.

Context. Our methodology arises from previous work on real-time operating systems modeling, embedded systems modeling and verification in the Polychrony workbench [START_REF] Berner | Modular design through component abstraction[END_REF] , a tool-set for embedded system design based on a multi-clocked synchronous model of computation and implemented by the data-flow notation Signal [START_REF] Benveniste | Synchronous programming with events and relations: the SIGNAL language and its semantics[END_REF] . In [START_REF] Gamati É | Synchronous modeling of avionics applications using the SIG-NAL language[END_REF] , the authors describe the implementation of a real-time operating system standard for avionics application: AR-INC [START_REF] Gamati É | Synchronous modeling of avionics applications using the SIG-NAL language[END_REF] . The commercial implementation of this library, RT-Builder from TNI-Valiosys, is used for industrial-scale embedded software engineering project in avionics.

In [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF] , this model is used to describe key services of the real-time Java virutal machine. It is applied to rethreading multi-threaded real-time Java programs by global optimization. In [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] , the application of our methodology to system-level design is further developped by studying its application to checking behavioral conformance between embedded systems described in SpecC and at heterogeneous levels of abstraction. In [START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF] , a generic translation scheme of SystemC programs to the Polychrony workbench is described by considering a static single assignement intermediate representation due to the GCC project [START_REF] Novillo | Tree SSA, a new optimization infrastructure for GCC[END_REF] . It is applied to design checking (e.g. race and lock detection). In [START_REF] Berner | Modular design through component abstraction[END_REF] , it is applied to modular verification by model checking and component-wise model abstraction.

We set our methodological framework within the general paradigm of a behavioral type system that associates meaning to software functionalities. The type system is cast in the generic programming language-oriented context of the three-address code (TAC) and static single assignment (SSA) intermediate representations (IR) of GCC.

RATIONALE

To allow for an easy grasp on the type system proposed for modeling behaviors, we outline the analysis of an imperative program, Figure 1, and depict the construction of its type, Figure 2. Figure 1 depicts a simple C code fragment consisting of an iterative program that counts the number of bits set to one in the variable idata. While idata is not equal to zero, it adds its right-most bit to an output count variable ocount and shifts it right in order to process the next bit. In the intermediate representation (IR) of the program (Figure 1, second column), all variables (idata and ocount) are read and written once per cycle. This IR can equally be one of the TAC and SSA formats of GCC. Label L2 is the entry point of the block associated with the while loop. The first instruction loads the input variable idata into the register T1. The second instruction stores the result of its comparison with 0 in the register T0. If T0 is false, control is passed to block L3. Otherwise, the next instruction is executed: the variable ocount is loaded into T2, the last bit of T1 is loaded into T3, the sum of T2 and T3 assigned to ocount and the right-shift of T1 assigned to idata. The block terminates with an unconditional branch back to label L2.

A behavioral type system. The meaning of this C program fragment is given in a minimalist formalism akin to Pnueli's synchronous transition systems [START_REF] Pnueli | Fair synchronous transition systems and their liveness proofs[END_REF] . It not only describes a behavior of the program suitable for its formal verification but also allows for global model transformations to be performed on it. Let us zoom on the block L2 in the example of Figure 2. The behavioral type of the block L2, middle, consists of the simultaneous composition of logical propositions that form a synchronous transition system. Each proposition is associated with one instruction: it specifies its invariants: it tells when the instruction is executed, what it computes, when it passes control to the next statement, when it branches to another block. On line 1 for instance, we associate the instruction T1 := idata to the proposition L2 ⇒ T1 := idata. The variable L2 is a boolean that is true iff the block of label L2 is being executed. Hence, the proposition says that, if the label L2 is being executed, then T1 is equal to idata. All propositions are conditioned by L2 to mean that they hold when block L2 is executed. The extent of a proposition is the duration of a reaction.

A reaction can be an arbitrarily long yet finite period of time provided that every variable or register changes its value at most once during that period. For instance, consider the instruction if T0 then L3. It is likely that label L3 will, just as L2, perform some operation on the input idata. Therefore, its execution is delayed until after the current reaction. We refer to L3 as the next value of the state variable L3, to indicate that it will be active during the next reaction. Hence, the proposition L2 ⇒ T0 ⇒ L3 says that control will be passed to L3 at the next reaction when control is presently at L2 and when T0 is true. The instructions that follow this test are conditioned by the negative ¬T0, this means: "in the block L2 and not in its branch to L3".

A BEHAVIORAL TYPE SYSTEM

The central element of the type system is a process. It consists of simultaneous propositions that manipulate signals. A signal is an infinite flow of values that is sampled by a discrete series of reactions. This series is called a clock. An event corresponds to the value carried by a signal during a reaction. The formal syntax of propositions in the behavioral type system is defined by the inductive grammar P. A propositon or process P manipulates boolean values noted v ∈ { false , true } and signals noted x, y, z. A location l refers to the initial value x 0 , the present value x and the next value x of a signal. A reference r is either a value v or a signal x.

(reference) r ::

= x | v (location) l ::= x 0 | x | x
A clock expression e is a proposition on boolean values that, when true, defines a particular period in time. The clocks 0 and 1 denote events that never/always happen. The clock x = r denotes the proposition: "x is present and holds the value r". Particular instances are: the clock x= def (x = x), which stands for "x is present"; the clock x= def (x = true ) for "x is true", and the clock ¬x= def (x = false ) for "x is false". Clocks are propositions combined using the logical combinators of conjunction e ∧ f , to mean that both e and f hold, disjunction e ∨ f , to mean that either e or f holds, and symmetric difference e \ f , to mean that e holds and not f .

(clock) e, f ::

= 0 | x = r | e ∧ f | e ∨ f | e \ f | 1
A process P consists of the simultaneous composition of elementary propositions. 1 is the process that does nothing. The proposition l = r means that "l holds the value r". The process e ⇒ P is a guarded command. It means: "if e is present then P holds". Processes are combined using synchronous composition P | | Q to denote the simultaneity of the propositions P and Q.

Restricting a signal name x to the lexical scope of a process P is written P/x. (process) P, Q :

:= 1 | l = r | x → l | e ⇒ P | (P | | Q) | P/x
An order of execution is imposed to a proposition by a scheduling constraint, noted x → l, to mean that "l cannot happen before x". Consequently, a proposition, e.g. x = y, is seen as the abstraction of an assignment, written x := y, defined by x = y | | y → x.

A synchronous model of computation

The meaning of our notation is given in the synchronous model of computation of [START_REF] Le Guernic | Polychrony for system design[END_REF] . We consider a partially-ordered set (T , ≤, 0) of tags. A tag t ∈ T denotes a symbolic period in time. The relation ≤ denotes a partial order and its minimum is noted 0. We note C ∈ C a chain of tags (a totally ordered subset of T ). We define an event e ∈ T × V by the pair of a value and a tag, a signal s ∈ S = {C → V |C ∈ C } by a function from a chain of tags C to values, a behavior b ∈ B = X S by a finite map from signal names X to signals S , a process p ∈ P by a set of behaviors of same domain. We write tags(s) for the tags of a signal s, b| X for the projection of a behavior b on X ⊂ X and b/X = b| vars(b)\X for its complementary, vars(b) and vars(p) for the domains of b and p. Example 1. Figure 3 depicts a behavior b over three signals named x, y and z. Two frames depict timing domains formalized by chains of tags. Signal x and y belong to the same timing domain: x is a down-sampling of y. Its events are synchronous to odd occurrences of events along y and share the same tags, e.g. t 1 . Even tags of y, e.g. t 2 , are ordered along its chain, e.g. t 1 < t 2 , but absent from x (we write t < t if t ≤ t and t ≤ t). Signal z belongs to a different timing domain. Its tags, e.g. t 3 are not ordered with respect to the chain of y, e.g. t 1 ≤ t 3 and t 3 ≤ t 1 .

x : Scheduling structure. To schedule the occurrence of events during a period or an instant t, we consider the fact that the pair x t of a time tag t and of a signal name x renders its very date d. The tag t represents the period during which the event takes place and the signal x its location. This consideration defines scheduling → by a pre-order relation between dates. Figure 4 depicts such a relation superimposed to the signals x and y of Figure 3.

• t 1 • • y : • t 1 • t 2 • • • z : • t 3 • • •
The relation y t 1 → x t 1 , for instance, requires y to be calculated before x at the period t 1 . A scheduling relation naturally satisfies containment with respect to the timing partial order ≤ of every signal x in a behavior b, in that for all t,t ∈ tags(b(x)), t < t naturally implies x t → b x t and, conver-

saly x t → b x t implies t < t. A scheduling relation is implicitly transitive (x t → b y t → b z t implies x t → b z t
) and its closure for restriction b/X is defined by x t → b/X y t iff x t → b y t and x, y ∈ X.

x :

• t 1 • • ↑ ↑ ↑ y : • t 1 • t 2 • • • Fig. 4.
Scheduling relations between simultaneous events.

Synchronous composition is noted p | | q and defined by the union of all behaviors b (from p) and c (from q) which are synchronous. All signals x shared by b and c belong to I = vars(p)∩vars(q) and are equal i.e. b| I = c| I : 6) is defined relatively to a given behavior b and consists of the set of tags satisfied by the proposition e in the behavior b. In Figure 6, the meaning of the clock

p | | q = {b ∪ c | (b, c) ∈ p × q, I = vars(p) ∩ vars(q), b| I = c| I }.   x : • t 1 • y : • t 1 • t 2 •   | |   y : • t 1 • t 2 • z : • t 3 •   =   x : • t 1 • y : • t 1 • t 2 • z : • t 3 •   Fig. 5. Synchronous composition of b ∈ p and c ∈ q.

Meaning of clocks.

The denotation [[e]] b of a clock expression e (table

[[0]] b = / 0 [[1]] b = tags(b) [[e ∧ f ]] b =[[e]] b ∩ [[ f ]] b [[e ∨ f ]] b =[[e]] b ∪ [[ f ]] b [[e \ f ]] b =b[[e]] b \ [[ f ]] b [[x = v]] b ={t ∈ tags(b(x)) | b(x)(t) = v} [[x = y]] b ={t ∈ tags(b(x)) ∩ tags(b(y)) | b(x)(t) = b(y)(t)}
x = v (resp. x = y) in b is the set of tags t ∈ tags(b(x)) (resp. t ∈ tags(b(x)) ∩ tags(b(y))) such that b(x)(t) = v (resp. b(x)(t = b(y)(t)). In particular, [[ x]] b = tags(b(x)).
The meaning of a conjunction e ∧ f (resp. disjunction e ∨ f and difference e \ f ) is the intersection (resp. union and difference) of the meaning of e and f . Clock 0 has no tags.

Meaning of propositions.

The meaning [[P]] e of a proposition P is defined with respect to a clock expression e. Where this information is absent, we assume [[P]] = [[P]] 1 to mean that P is an invariant (and is hence independent of a particular clock). The meaning of an initialization [[x 0 = v]] e consists of all behaviors defined on x, written b ∈ B| x such that the initial value of the signal b(x) equals v. Notice that it is independent from the clock expression e provided by the context. We write B| X for the set of all behaviors of domain X, min(C) for the minimum of the chain of tags C, succ t (C) for the immediate successor of t in the chain C, vars(P) and vars(e) for the sets of signal names of P and e.

[[x = y]] e ={b ∈ B| vars(e)∪{x,y} | ∀t ∈ [[e]] b , t ∈ tags(b(x)) ∧ t ∈ tags(b(y)) ∧ b(x)(t) = b(y)(t)} [[y → x]] e ={b ∈ B| vars(e)∪{x,y} | ∀t ∈ [[e]] b , t ∈ tags(b(x)) ⇒ t ∈ tags(b(y)) ∧ y t → b x t } [[x = y]] e ={b ∈ B| vars(e)∪{x,y} | ∀t ∈ [[e]] b , t ∈ C = tags(b(x)) ∧ t ∈ tags(b(y)) ∧ b(x)(succ t (C)) = b(y)(t)} [[y → x ]] e ={b ∈ B| vars(e)∪{x,y} | ∀t ∈ [[e]] b , t ∈ C = tags(b(x)) ⇒ t ∈ tags(b(y)) ∧ y t → b x succ t (C) } [[x 0 = v]] e ={b ∈ B| x | b(x)(min(tags(b(x)))) = v} [[ f ⇒ P]] e =[[P]] e∧ f [[P | | Q]] e = [[P]] e | | [[Q]] e [[P/x]] e = [[P]] e /x

AN INTERMEDIATE REPRESENTATION

We are now equipped with the required mathematical framework to address the modeling of embedded systems described by communicating program threads. This model is described in terms of a type inference system and extended to the structuring elements of a generic module system. This framework allows to give a behavioral signature of the component of the system, compositionally check the correct composition of such components to form architecture, to optimize the described software elements from the imposed hardware elements by, first, detaching the formal model from the functional architecture description and, second, using the model to regenerate an optimized software matching the requirements of the execution architecture.

Formal syntax. Imperative programs are represented in an intermediate form that is common to the TAC and SSA IRs of GCC which provides language-independence and local optimization. A program pgm consists of a sequence of labeled blocks L:blk. Each block consists of a label L and of a sequence of statements stm terminated by a return statement rtn. Block instructions consist of native method invocations x = f ( 1..n ), lock monitoring and branches if x then L. Blocks are returned from by either a goto L, a return or an exception throw x. The declaration catch x from L 1 to L 2 using L 3 that matches an exception x raised at block L 1 activates the exception handler L 3 and continues at block L 2 .

= x = f (y 1..n ) | if x then L (return) rtn ::= goto L | return x | throw x | catch x from L to L using L
In the remainder, we only assume that a block always starts with a label and finishes with a return statement: stm 1 ; L:stm 2 is rewritten as stm 1 ; goto L; L:stm 2 . A call x = f (y) to a possibly blocking external method f , such as wait x in SystemC or Java, is always placed at the beginning of a block L. For instance, stm 1 ; wait x; stm 2 is rewritten as stm 1 ; goto L; L:wait v;stm 2 . By contrast, primitive operations x = f (y, z) are assumed to take an insignificant amount of time and are executed with the normal control-flow of the block.

Example 2. To outline the construction of the intermediate representation of a program, let us reconsider the example of Section 2 and detail the function that counts the number of bits set to 1 in a bit-array data (Figure 9). It consists of three blocks. The block labeled L1 waits for the signal lock before initializing the local state variable idata to the value of the input signal data and ocount to 0. Label L2 corresponds to a loop that shifts idata right to add its right-most bit to ocount until termination (condition T0). In the block L3, ocount is sent to the signal count and lock is unlocked before going back to L1. The SSA form of the program differs in the function-wise guarantee that all variable be assigned once during an execution cycle. It consists of performing assignments to idata and ocount in blocks L1 and L2 to temporary variables and branch to a merge block L4 where the appropriate copy is assigned to the variable upon the value of a boolean condition φ (to mean from L1 or not). For an instruction stm, the function stm E L 1 L 2 takes two labels which represent the entry label L 1 of the statement and its continuation by the pseudo-label L 2 . The denotation of a function call x = f (x 1..k ) is that given by E for the variable names x 1..k x and the entry and exit labels L 1 and L 2 .

Meaning of instructions. The denotation of instructions

The meaning of an if x then L 1 instruction consists of all behaviors b defined on x, L 1 , L 2 and L 3 which share the same chain of tags C and such that, if b(L 1 )(t) is true, then the continuation label L 3 is active iff x if false, i.e. b(L 3 )(t) = ¬b(x)(t); and if x is true then L 2 is active next, i.e. b(x)(t) true implies b(L 2 )(succ t (C)) true. For a return instruction rtn, the denotation function rtn E L only takes one (entry) label L. The meaning of return x, goto L and throw x instructions are given using the same principle as for the if x then L. Notice the introduction of a pseudo-label to handle a sequence of instructions. The meaning of a sequence stm; blk starting at block L 1 is defined by using a local peudo-label L 2 to denote the continuation of stm by stm E L 1 L 2 and hence the entry point of blk by blk E L 2 . The meaning of the sequence is finalized by synchronous composition and the scope of L 2 restricted to it. The meaning of a program L : blk; pgm is similar yet simpler as there is no continuation between blocks. The meaning of a function declaration m f (x 1...k ) {pgm} is listed just to show the order in which the argument, result, entry and exit label names are used to parameterize the meaning of the function body.

x = f (x 1..k E L 1 L2 =E( f )(x 1..k xL 1 L 2 ) if x then L 1 E L 2 L 3 ={b ∈ B| xL 123 | ∀t ∈ C = chain b (xL 123 ), b(L 1 )(t) ⇒ (b(L 3 )(t) = ¬b(x)(t) b(x)(t) ⇒ b(L 2 )(succ t (C)))} return x E L ={b ∈ B| Lxy |E(return) = y, ∀t ∈ C = chain b (Lxy), b(L)(t) ⇒ b(y)(t) = b(x)(t)} goto L 1 E L 2 ={b ∈ B| L 1 L 2 | ∀t ∈ C = chain b (L 1 L 2 ), b(L 2 )(t) ⇒ b(L 1 )(succ t (C))} throw x E L ={b ∈ B| Lx |∀t ∈ C = chain b (Lx), b(L)(t) ⇒ b(x)(t)} stm; blk E L 1 =( stm E L 1 L 2 | | blk E L 2 )/L 2 L : blk; pgm E = blk E L | | pgm E m f (x 1...k ) {pgm} E =E[ f : λ x 1..k xyy exit .(p/L 1.. j )] | p = pgm E[return:y] ∧ labs(pgm) = L 1.. j

BEHAVIORAL TYPE INFERENCE

The behavioral type inference system is defined by induction on the formal syntax of programs pgm. To define it, we assume that the finite set L of program labels L. To each block of label L, the inference system associates a boolean proposition L of the same name, called the input clock, and a boolean proposition L exit , called its output clock. The proposition L is true iff the block L is active during a given transition. The proposition L exit is true iff the execution of block L terminates during a given transition. The relation defined by the behavioral type system has the form: e 0 , E L : blk : P, e 1 where e 0 denotes the input clock of the block of instructions blk, L is its label, P the proposition to denote its behavior, and e 1 its output or continuation clock. The type environment E gives the behavior of methods and functions defined in the context of the program. It associates a variable x to a type m (a class name), a class name m to a class type T (described in the next section) and a method f to a proposition P and an output clock e parameterized by the sequence x 1..n formed of its input and output variables and input clock name (see rule (8) below).

E ::= [] | E [x : m] | E [m : T ] | E [ f : λ ( 1..n ). P, e ]
Rules (1-8) define the behavioral type inference system. Rules (1-2) are concerned with the iterative decomposition of a program pgm into blocks blk and with the decomposition of a block into statements stm and return instruction rtn.

(1)

L, E L : blk : to mean that the next value of L 2 is true when e is active and when x is true.

P E pgm : Q E L : blk; pgm : P | Q Notice that,
(3) e, E L :

if x then L 1 : (e ∧ x) ⇒ (L exit | | L 1 ), e ∧ ¬x
All return instructions, rules (4-7), define the output clock L exit of the current block L by the input clock e. This is the right place to do that: e defines the condition upon which the block actually reaches its return statement.

A goto L 1 instruction, rule (4), passes control to block L 1 unconditionally at the input clock e.

(4) e, E L : goto

L 1 : e ⇒ (L exit | | L 1 )
A return instruction, rule (5), fetches the variable y used as return variable for the current method or function and sets y exit to true at clock e in order to notify the caller that the method terminates execution. 2. On the first line, for instance, we associate the instruction T1 = idata of block label L2 to the proposition L2 ⇒ T1 = idata. In this proposition, the variable L2 is a boolean that is true iff the block L2 is being executed. So, the proposition says that, if L2 is being executed, then T1 is always equal to idata. If it not, another proposition may hold. All subsequent propositions are conditioned by L2 to mean that they hold when L2 is executed. Next, consider the instruction if T0 then L3. Its invariant L2 ⇒ T0 ⇒ L3 says that control passes to L3 when control is presently at L2 and when T0 is true. The instructions that follow this test are conditioned by the negative ¬T0, this means: "in the block L2 and not in its branch to L3". The catch statement catch x from L to L 1 using L 2 matching rule (6), passes control in rule (7) to the exception handler L 2 and then to the block L 1 upon termination of L 2 notified by L exit 2 . This requires, first, to activate L 2 from L when x is present and then to pass the control to L 1 upon termination of the handler.

(7) e, E L : catch xto L 1 using L 2 : ( x ∧ L exit ) ⇒ L 2 | | L 2 exit ⇒ L 1
Rule (8) is concerned with type assignement for native and external method invocations x = f (x 1..k ). The generic type of f is taken from an environment E ( f ). It is given the name of the actual parameters x 1...k , of the result x and of the input clock e. E ( f )(x 1...k xe) yields the corresponding behavioral type P, e 1 .

(8) e, E L :

x = f (x 1...k ) : E ( f )(x 1...k , x, e)
Example 4. As an example, the wait-notify protocol used in SystemC of Java to arbiter access to shared data is modeled using a boolean flip-flop variable x. The notify method defines the next value of the lock x by the negation of its current value at the input clock e. The wait method continues activates iff the value of the lock x has changed at the input clock L: L ∧ (x = x ). Otherwise, at the clock L ∧ (x = x ), the control is passed to L by a delayed transition e \ ŷ ⇒ L .

E (notify) = λ xe. e ⇒ (x = ¬x), e E (wait) = λ xL. L ∧ (x = x ) ⇒ L , L ∧ (x = x )
Consider the wait-notify protocol at blocks L1 and L3, Figure 13. The wait instruction continues if L1 receives control and if the lock is toggled (proposition lock = lock ). If so, the block is executed and control passes to the block L2 and, if not, to the block L1.

= [[E ]] then b ∈ [[P]] 1 iff b ∈ pgm E
From TAC to SSA. The type system and its semantics rely on the property of the TAC IR that every variable is defined at once within a block (this hypothesis is sound for a program in SSA form as well). As a consequence, each block delimits an atomic reaction in the type system and, therefore, transition from a block to another cannot be immediate (by saying L for "label L is active") but delayed (by saying L for "label L will be active next time"). In SSA, this guarantee is provided for the whole "text" of the function. In particular, for a goto from a block L 1 to a block L 2 textually after L 1 (written L 1 < L 2 ), SSA guarantees that all variables defined in L 1 are different from those in L 2 . This is of course not the case for a loop, in which case we have L 1 ≥ L 2 . To take advantage of this additional guarantee, our type inference system can be refined by considering the following rule to handle gotos (and similarly, if-thens and throw-catchs). It consists of activating the target block L 2 immediately.

(4b) L 1 < L 2 e, E L 1 : goto L 2 : e ⇒ (L 1 exit | | L 2 )
The translation of the EPC in SSA form using rule (3b) outlines the benefits of this optimization. The resulting type has strictly fewer delayed transitions: one to L2 in L3 and another to L1 in L4. All other transitions are immediate and considered within the same reaction.

considered in [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] to be easily implemented. Checking the correct refinement of an initial module, of type P, by its upgrade, of type Q, amounts to checking that the final guarantee Q satisfies the initial assumptions P.

In [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] , this is implemented by compositionally model checking that Q is finitely flow-equivalent to P. Figure 15 describes a typical case study of conformance checking. We consider the refinement of the C model of an even parity checker (EPC) from a high-level design abstraction, left, where communication is abstracted by shared variables and a lock, to an architecture-level design abstraction, right, where the communication medium is refined by the insertion of a channel implementing a double handshake protocol, Figure 16. Checking conformance of the architecture-level design with respect to its system-level abstraction amounts to checking that both designs are flow equivalent. The very notion of flow equivalence under consideration con-sists is defined in the asynchronous structure of our model of computation that is presented next. x : 17 illustrates two asynchronously equivalent behaviors related by relaxation. The first event along x has been shifted (and its scheduling constraint with an initially synchronous event along y lost) as the effect of finitely delaying its transmission. Asynchronous composition is noted p q and defined using the partial-order structure induced by the relaxation relation. The composition of p and q consists of behaviors d that are relaxations of behaviors b and c from p and q along shared signals I = vars(p) ∩ vars(q), i.e. b| I d| I c| I , and that are stretching of b and c along the independent signals of p and q, i.e. b/I ≤ d/I ≥ c/I.

• t 1 • • ↑ ↑ ↑ y : • t 1 • t 2 • • • x : • t 3 • • y : • t 4 • t 5 • • • Fig. 17
  x : • t 1 • t 3 y : • t 2 • t 4     x : • t 1 • t 2 y : • t 1 • t 2 z : • • •     x : • • y : • • z : • • •   Fig. 18. Asynchronous composition.
Figure 18 illustrates the asynchronous composition of a behavior b and of a behavior c. Signals x and y are alternated in b, left, and synchronous in c, middle. Asynchronous composition allows x and y to be independently stretched in b and c in order to find a common flow in the asynchronous composition, right.

Flow preservation

To check the existence of a flow-preserving timing relation between the two systems outlined in the previous section, the refinement-based methodology similar of [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] shows that the types P and Q of Figure 15 are finitely flow-equivalent. To this end, we formulate the timing deformation allowed by finite buffering protocols starting from the model of a one-place FIFO buffer which we will use to draw the spectrum of possible timing relations under consideration. Figure 19 depicts the timing deformation allowed along a signal x by a one place buffer.

y : • t 1 • t 2 • • • ↓ ↓ ↓ x : • t 1 • • x 1 y : • t 1 • t 2 • • • -→ ↓ -→ x : • t 3 • •
(1) t ∈ tags(d(x)) ⇒ d(x)(t) = d(m)(t) ∧ x t → d m t (2) t ∈ tags(d(x)) ⇒ d(m)(t) = d(m)(pred C (t)) (3) t ∈ tags(c(x)) ⇒ c(x)(t) = d(m)(t) ∧ ∀y ∈ vars(d) \ m, y t → d x t (4) t ∈ tags(c(x)) ⇒ c(x)(t) = d(x)(t) ∨ c(x)(succ C (t)) = d(x)(t)
For all t ∈ C, rule (1) says that, when an input d(x) is present at some time t, then d(m) takes its value. If no input is present along x at t, rule (2), then d(m) takes its previous value. Rule (3) says that, if the output c(x) is present at t, then it is defined by d(m)(t). Finally, rule (4) requires this value to either be the present or previous value of the input signal d(x), binding the size of the buffer to one place.

d(x) : • • • • ↓ (1) ↓ (1) ↓ (1) ↓ (1) d(m) : • • -→ (2) • • • -→ (2) • ↓ (3) ↓ (3) ↓ (3) ↓ (3) c(x) : • • • • (4) (4) (4) (4)
Fig. 20. Timing and scheduling relations through finite relaxation.

Definition 1 accounts for the behavior of bounded FIFOs in a way that preserves scheduling relations. It implies a series of (reflexive-antisymmetric) relations n (for n > 0) which yields the (series of) reflexivesymmetric flow relations ≈ n to identify processes of same flows up to a flow-preserving first-in-first-out buffer of size n.

A compositional methodology

We say that a process P is finitely flow-preserving iff given finitely flowequivalent inputs, it can only produce behaviors that are finitely flow equivalent.

Definition 2 (finite flow-preservation).

P is finitely flow-preserving with I ⊂ in(P) iff for all behaviors b, c of

[[P]], if (b| I )≈(c| I ) then b/I ≈ * c/I.
Example of finitely flow-preserving processes are endochronous processes [START_REF] Le Guernic | Polychrony for system design[END_REF] . An endochronous process which receives flow equivalent inputs produces clock-equivalent outputs. It hence forms a restricted subclass of finitely-flow preserving processes. Furthermore, notice that flowpreservation is stable to the introduction of a wrapper of P consisting of a finite FIFO buffering protocol. A refinement-based design methodology based on the property of finite flow-preservation consists of characterizing sufficient invariants for a given model transformation to preserve flows.

Definition 3 (finite flow-invariance).

The

transformation of P into Q such that I ⊂ in(P) = in(Q) is finitely flow-invariant iff ∀b ∈ [[P]], ∀c ∈ [[Q]], (b| I )≈ * (c| I ) ⇒ b ≈ * c
The property of finite flow-invariance is a very general methodological criterion. For instance, it can be applied to the characterization of correctness criteria for model transformations such as protocol insertion or desynchronization. Let P and Q be two finitely flow-preserving processes and R a protocol to link P and Q, such as a finite FIFO buffer, or a double hand-shake protocol, or a relay station [START_REF] Carloni | Latency-Insensitive Protocols[END_REF] , or a loosely time-triggered architecture [START_REF] Benveniste | A protocol for loosely time-triggered architectures[END_REF] . In definition 4, we write b[x/y] for the behavior resulting of substitution of the signal name y by the signal name y in the domain of the behavior b and [x i /y i ] 0<i≤n for the compposition of n substitutions.

Definition 4 (flow-preserving protocol).

The process R is a flow-preserving protocol iff there exists n > 0 such that inputs in(R) = {x 1..n } are finitely flow-equivalent to outputs out(R) = {y 1..n }, i.e., ∀b ∈

[[R]], b| x 1..n ≈ * (b| y 1..n [x i /y i ] 0<i≤n )
The wrapper R P of a process P with a protocol R is defined by redirecting the signals of P to R. In definition 5, this redirection is modeled by substituting signal names: we write P[x/y] for the process resulting of substituting y by x in P.

Definition 5 (wrapper).

Let P be a process such that in(P) = {x 1..m } and out(P) = {x m+1..n }. Let R be a flow-preserving protocol such that in(R) = {y 1..n } and out(R) = {z 1..n }. The wrapper of P with R is the template process noted R P and defined by:

R P def = ((R[x i /z i ] m<i≤n ) [x i /y i ] 0<i≤m ) | | (P[y i /x i ] m<i≤n ) [z i /x i ] 0<i≤m /y 1..n z 1..n
A sufficient condition for the insertion of a protocol between two synchronous processes P and Q to finitely preserve flow is to guaranty that P| I | | Q| I is finitely flow preserving for I = vars(P) ∩ vars(Q), meaning that all communications between P and Q via a shared signal x ∈ I should be flow preserving and that P and Q may otherwise evolve independently.

Property 2 (protocol insertion).

If R is a flow-preserving protocol and P is finitely flow-preserving then R P is finitely flow-preserving. If R is a flow-preserving protocol and P, Q, P| I | | Q| I are finitely flow-preserving then R P | | R Q is finitely preserving (I = vars(P) ∩ vars(Q)).

FURTHER APPLICATIONS

We have introduced a type system allowing to model the control and data flow graphs of a given imperative program in intermediate form. Applications of the proposed type system encompass optimization and verification issues encountered in system design.

Rethreading

Because our type system entirely model the control and data-flow of application components and architecture functionalities, one can operate global optimization on the whole model of the application. Signal, in particular, implements the notation of our type system using data-flow equations and allows for the generation of sequential code by employing a global controlflow graph transformation called hierarchization [START_REF] Amagbegnon | Implementation of the data-flow synchronous language SIGNAL[END_REF] . Hierarchization consists of hooking elementary control flow graphs (in the form of if-then-else structures). For instance, let h3 be a clock computed using h1 and h2 and h be the head of a tree in which h1 and h2 are computed. Then h3 can computed after h1 and h2 and placed under h.

Example The implications of hierarchization for code generation can be outlined by considering the specification of one-place buffer. The process buffer has input x, output y and implements two functionalities.

> def = r 0 = b | | r := x | | x ⇒ y := x | | ŷ \ x ⇒ y := r
We observe that s defines the master clock of buffer. There are two other synchronization classes, x and y, that corresponds to the true and false values of the boolean flip-flop variable s, respectively. This defines three nodes in the control-flow graph of the generated code (Figure 21). At the master clock ŝ, the value of s is calculated from zs, its previous value. At the subclock s = x, the input signal x is read. At the sub-clock ¬s = ŷ the output signal y is written. Finally, the new value of zs is determined. Operating this transformation on the model of a multi-threaded application results in merging all threads into a single control-flow graph whose scheduler foot-prints sequentially processes each elementary execution block upon a particular condition. In [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF] , we report a 300% average speedup resulting of applying this optimization to real-time Java programs compared to their execution using a commercial compiler.

Module checking

In [START_REF] Talpin | A behavioral type inference system for compositional system design[END_REF] , we define a behavioral module checking algorithm based on similar principles as those exposed in the previous section. This system allows to give guarantees As an example, consider a SystemC class m 0 whose virtual fields are the clocks x, y and a procedure f . Assume an explicit behavioral type declaration #TYPE( f , Q) which associates f with a description of its behavior: the proposition Q denotes its expected functionality. Let us associate the interface m 0 with the class parameter m 1 of a template class m 2 . The interface m 0 now gives a behavioral type to the method f in the class parameter m 1 expected by the module m 2 . The assumption Q on the behavior of m 1 . f is required to provide a guarantee on the behavior of the module m 2 produced by the template class. Module m 3 is a candidate parameter for m 2 . It structurally implements the interface m 0 and is annotated with the guarantee #TYPE( f , P), where P is the type of pgm. Now, let m 4 be the class defined by the instantiation of the template m 2 and the parameter m 3 . To check the compatibility of the actual parameter m 3 with the formal parameter m 0 , we check the containment of the behaviors denoted by the proposition P (the type of the actual parameter) in the proposition Q (the type of the formal parameter). This amounts to check that P implies Q, either by model checking (if Q contains state transitions) or by static checking (if Q is a "stateless" property). We consider a simple and minimalistic module system model for the purpose of exemplifying the scalability of our technique to structuring elements of general-purpose languages such as Java, C++ or SystemC. A component mod in an architecture is a class definition class m {dec}, a template declaration template class x : m mod or a sequence of modules mod; mod. A class consists of a sequence of declarations. The keyword use m allows to use the members of class m within the current module (hence name elaboration is assumed to be explicit for simplification purposes). Declarations dec associate locations x with native classes m or template class instances m m 1..k and methods with a name f and a definition pgm. For instance, integer x defines an integer variable x (in Java or C) while sc signal boolean x defines a boolean signal x in SystemC. As we focus on typing program module behaviors we assume no sub-typing relation between data-types. We define our module system starting from the behavioral type system of Section 5. The type T of a module m consists of an environment E (that associates functions f with behaviors and variables x with data-types) and of a proof obligation C . The type T 1 → T 2 denotes a template class that produces a module of type T 2 given a parameter of type T 1 . It defines the proposition P and the continuation or output clock x exit of the method f parameterized by its sequence x 1..k of input variables, its result variable x, and the label L that defines its input clock. To process the function, we associate its reutrn value, denoted by return to a signal x used to carry its value.

class m 0 { virtual sc clock x, y; virtual void f () {} #TYPE( f , Q) }; template class m 1 #TYPE(m 1 , m 0 ) SC MODULE(m 2 ) { SC CTOR(m 2 ) { SC THREAD(m 1 . f ) sensitive x } }; class m 3 { sc clock x, y; void f () { pgm} #TYPE( f , P) }; m 2 m 3 m 4 ;
(c) L, E [return : x] L : blk; pgm :

P ( * ) E m f (x 1...k ) {pgm} : [ f : λ x 1..k xL. P/L , x exit ]
Rule (d) sequentially processes the declarations dec in a module. The constraint true is omitted in rules (a) and (c).

(d)

E dec 1 :

E 1 /C 1 E E 1 dec 2 : E 2 /C 2 E dec 1 ; dec 2 : E 1 E 2 /C 1 ∧ C 2
m is T [m 2 /x] (x is substituted by m 2 ). (β ) E m 1 : Λ(x : T 1 ).T E m 2 : T 2 T 1 ≤ T 2 ⇒ C E m 1 m 2 m : ([m : T ]/C )[m 2 /x]
Rule (γ) defines the type of a template declaration template class m 1 : n 1 mod. Provided the assumption that the formal parameter m 1 of the template has the type T 1 (that of the virtual class name n 1 ) the template guarantees that the module m 2 it defines has type T 2 . Hence the type Λ(m 1 : T 1 ).T 2 for module m 2 .

(γ)

E n 1 : T 1 E [m 1 : T 1 ] mod : [m 2 : T 2 ] E template class m 1 : n 1 mod : [m 2 : Λ(m 1 : T 1 ).T 2 ]
Rule (δ ) processes module declarations in sequence.

(δ )

E mod 1 :

E 1 /C 1 E E 1 mod 2 : E 2 /C 2 E mod 1 ; mod 2 : E 1 E 2 /C 1 ∧ C 2
Finally, the resolution of the behavioral sub-typing relation T 1 ≤ T 2 is defined by structural induction. It reduces to the proof of a conjunction of propositions P 1 ⇒ P 2 .

Design checking

Properties pertaining on common design errors can easily be expressed and checked using our type system. Whereas related approaches consist of proposing an ad-hoc type system for analyzing a specific pattern of design errors: race conditions, deadlocks, threads termination; and in a given programming language: Java, C, SystemC, our type system provides a generic framework to perform verification via model checking of behavioral properties of embedded systems described using imperative programming languages.

Termination. A common design error found in embedded system design is the unexpected termination of a thread due to, e.g., an uncaught exception. Here, the termination of a thread f can simply be expressed by the accessibility of the property f exit = 1. Unexpected termination can hence be avoided by checking that f satisfies f exit = 0.

Deadlocks. Another common design error is a wait statement that does not match a notification and yields the thread to block. Let L 1...n be the clocks of the blocks L 1...n in which a lock x is notified. Waiting for x at a given label L eventually terminates if P satisfies L ∧ ¬(∧ n i=1 L i ) = 0. Races. Similarly, concurrent write accesses to a variable x shared by parallel threads can be checked exclusive by considering the input clocks e 1,..n of all write statements x = f (y, z) by verifying that P satisfies (e i ∧ (∨ j =i e j )) = 0 for all 0 < i ≤ n.

Larger case-studies reporting applications of our technique in system design and verification are the complete model of a finite input response (FIR) filter starting from the SystemC 2.0.1 distribution [START_REF] Berner | Modular design through component abstraction[END_REF] . In this case study, we demonstrate the benefits of modularly associating each System module to a behavioral type interface to perform optimizations and verifications which are modular and yet sensitive to the architecture in which modules or components are placed as reflected by the architecture's behavioral type and by application of an assumption-guarantee reasoning principle. A more recent and larger experiment applies the principles presented in this article to co-modeling by considering predefined SystemC components and connecting them around a bus architecture by giving a synchronous data-flow model of the interconnection wrappers.

RELATED WORK

By contrast to traditional type systems, which focus on rendering datastructure abstractions, behavioral type systems [START_REF] Nielson | Type and Effect Systems: Behaviours for Concurrency[END_REF][START_REF] Rajamani | A behavioral module system for the π-calculus[END_REF] are concerned with the abstraction of control structure in concurrent programs.

A related direction of research is software model checking using popular tools like Bandera [START_REF] Hatcliff | Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software[END_REF] , Mops [START_REF] Chen | Model Checking One Million Lines of C Code[END_REF] , Verisoft [START_REF] Godefroid | Software Model Checking: The VeriSoft Approach[END_REF] , Modex [START_REF] Holzmann | Software Model Checking[END_REF][START_REF] Holzmann | An automated verification method for distributed systems software based on model extraction[END_REF] , Slam [START_REF] Ball | Refining Approximations in Software Predicate Abstraction[END_REF] , CBMC [START_REF] Kroening | A Tool for Checking ANSI-C Programs[END_REF] , Magic [START_REF] Chaki | Modular Verification of Software Components in C[END_REF] , Blast [START_REF] Beyer | The Blast query language for software verification[END_REF] , Pathfinder [START_REF] Visser | Model Checking Programs[END_REF] . Most software model checking tools proceed by extracting temporal logic models of source programs (either Java or C but raraely both) and perform sophisticated and efficient abstractions to drastically accelerate property verification.

Our approach contrasts with the software model checking trend in that it is primarily aimed at modeling software and then perform either of global model transformations (desynchronization, rethreading, etc) and code generation [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF] , conformance checking by finite-flow equivalence using model checking techniques [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] or modular state-less abstraction for efficient property verification [START_REF] Berner | Modular design through component abstraction[END_REF] . As such, our approach most closely relates to that of Modex [START_REF] Holzmann | An automated verification method for distributed systems software based on model extraction[END_REF] in which temporal property models are extracted for later verification with Spin. We experienced that representing such models using executable specifications expressed in a multi-clocked synchronous model offers the additional benefit of operating orrectnesspreserving model transformations such as protocol synthesis (desynchronization [START_REF] Talpin | Formal refinement checking in a system-level design methodology[END_REF] ) or static scheduling (rethreading [START_REF] Talpin | Hard real-time implementation of embedded software in JAVA[END_REF] ). Finally, and unlike most related approaches in SMC, which are geared towards a particular programming language, we focus on a language-independent intermediate representation of Gnu's GCC.

We share the aim of a scalable and correct-by-construction exploration of abstraction-refinement of system behaviors with the work of Henzinger et al. on interface automata [START_REF] De Alfaro | Interface theories for component-based design[END_REF] . Our approach primarily differs from interface automata in the data-structure used in the Polychrony workbench: clock equations, boolean propositions and state variable transitions express the multi-clocked synchronous behavior of a system. Compared to an automata-based approach, our declarative approach allows to hierarchically explore abstraction capabilities and to cover design exploration with the methodological notion of refinement along the whole design cycle of the system, ranging from the early requirements specification to the latest sequential and distributed code-generation [START_REF] Le Guernic | Polychrony for system design[END_REF] .

CONCLUSIONS

Our contribution contrasts from related studies by the capability to capture a complete behavioral model of the type-checked system as well as model abstractions expressed at a scalable degree of precision. In our type system, scalability ranges from the capability to express the exact meaning of the program, in order to make structural transformations and optimizations on it (just as in a traditional type system), down to properties expressed by boolean equations between clocks, allowing for a rapid static-checking of design correctness properties. Our system allows for a wide spectrum of design abstraction and refinement patterns to be applied on a model, e.g. abstraction of states by clocks, abstraction of existentially quantified clocks, hierarchic abstraction, in the aim of choosing a better degree of abstraction for faster verification.

The main novelty in our approach is the use of a multi-clocked synchronous formalism to support the construction of a scalable behavioral type inference system for de facto standard design and programming languages, and the materialization of a companion refinement-based design methodology imposed through the strong typing policy of a module system, that reduces compositional design correctness verification to the vali-dation of synthesized proof obligations. The proposed type system allows to capture the behavior of an entire system-level design and to re-factor it, allowing to modularly express a wide spectrum of static and dynamic behavioral properties, and to automatically or manually scale the desired degree of abstraction of these properties for efficient verification. The type system is presented using a generic and language-independent intermediate representation. It operates transformations implemented in the platform Polychrony, to perform refinement-based design exploration. It yields to SAT and model checking verification tools for an efficient verification of expected design properties and an early discovery of design errors.

Fig. 1 .

 1 Fig. 1. From a C-like program to its intermediate representation.

Fig. 2 .

 2 Fig. 2. From a generic intermediate representation to propositions.

Fig. 3 .

 3 Fig. 3. behavior b over three signals x, y and z in two clock domains.

Fig. 6 .

 6 Fig. 6. Denotational semantics of clocks.

Fig. 7 .

 7 Fig. 7. Denotational semantics of propositions.

  (program) pgm ::= L:blk | pgm; pgm (block) blk ::= stm; blk | rtn (instruction) stm ::

Fig. 8 .

 8 Fig. 8. Syntax for an intermediate representation of imperative programs.

Fig. 9 .

 9 Fig. 9. From three address code ...

  Fig. 10. ... to static single assignment.

Fig. 11 .

 11 Fig. 11. Denotational semantics of instructions.

( 5 )

 5 E (return) = y e, E L : return x : e ⇒ (L exit | | y exit | | y := x) A throw x instruction, rule (6), produces an event along the signal x at the input clock e by e ⇒ x.

( 6 )Example 3 .

 63 e, E L : throw x : e ⇒ (L exit | | x) Let us zoom on the block L2 of Figure

Fig. 12 .

 12 Fig. 12. Modeling control flow in an imperative program.

Fig. 15 .

 15 Fig. 15. Conformance-checking the refinment of an even-parity checker.

Fig. 16 .

 16 Fig.16. Refinement of locks with a double handshake protocol.

6. 1 .

 1 Asynchronous structure The asynchronous structure of polychrony is modeled by weakening the clock-equivalence relation to allow for comparing behaviors whose successive values match regardless of time: two behaviors are flow-equivalent iff their signals hold the same values in the same order. The relaxation relation allows to individually stretch the signals of a behavior in a way preserving scheduling constraints. A behavior c is a relaxation of b, written b c, iff vars(b) = vars(c) and, for all x ∈ vars(b), b| {x} ≤ c| {x} .

  Fig. 17. Relating asynchronous behaviors by relaxation. Relaxation is a partial-order relation which defines flow-equivalence: b and c are flow-equivalent, written b ≈ c, iff there exists a behavior d s.t. d b and d c.Figure17illustrates two asynchronously equivalent behaviors related by relaxation. The first event along x has been shifted (and its scheduling constraint with an initially synchronous event along y lost) as the effect of finitely delaying its transmission. Asynchronous composition is noted p q and defined using the partial-order structure induced by the relaxation relation. The composition of p and q consists of behaviors d that are relaxations of behaviors b and c from p and q along shared signals I = vars(p) ∩ vars(q), i.e. b| I d| I c| I , and that are stretching of b and c along the independent signals of p and q, i.e. b/I ≤ d/I ≥ c/I.

Figure

Fig. 19 .Definition 1 (

 191 Fig.19. Relation between events through a one place buffer along x.

  We write b 1 c iff b x 1 c for all x ∈ vars(b), and, for all n > 0, b n+1 c iff there exists d such that b 1 d n c. The largest equivalence relation modeled in the polychronous model of computation consists of behaviors equal up to a timing deformation performed by a finite FIFO protocol: b and c are finitely flowequivalent, written b ≈ * c, iff there exists n > 0 and d s.t. d n b and d n c.

  buffer < x, y > def = alternate < x, y > | | current < x, y > One is the process alternate which desynchronizes the signals x and y by synchronizing them to the true and false values of an alternating boolean signal s. alternate < x, y > def = s 0 = true | | x = s | | ŷ = ¬s | | s := ¬s The other functionality is the process current. It defines a cell in which values are stored at the input clock x and loaded at the output clock ŷ. current < x, y, b

Fig. 21 .

 21 Fig. 21. C code generated for the one-place buffer specification.

Fig. 22 .

 22 Fig. 22. Type assumptions and guarantees in the SystemC module system.

  Fig. 23. Abstract syntax for declarations and modules.

  (type) T ::= E /C | Λx : T 1 .T 2 A proof obligation is a conjunction of propositions of the form P ⇒ Q. A proof obligation P ⇒ Q is incurred by the instantiation of a template class, whose formal parameter has type P and by an actual class parameter, of type Q. (obligation) C ::= true | P ⇒ Q | C ∧ C The synthesis of proof obligations pertaining on the correctness of module composition is defined by the relation E mod : E /C and by induction on the syntax of modules and declarations. Rule (a) associates the location x with the type name m in the class-field type [x : m]. Rule (b) allows to use or open a module m. (a) E m x : [x : m] (b) E [m : T ] use m : T Rule (c) associates a method definition f with the class-field type [ f : λ x 1..k xL. P, x exit ]. Its side-condition ( * ) is that L = labs(pgm) is the set of labels defined in pgm and that L = start(pgm) is the entry point of pgm.

Class-field declarations

  contribute to building the type T of a module. We write E m : T iff E contains [m : T ]. An extension noted E 1 E 2 is defined by E 2 and all class names and class-field names of E 1 not overridden by a declaration in E 2 . Rule (α) defines the type T of a class by that of its field declarations. (α) E dec : T E class m {dec} : [m : T ] Rule (β ) defines the type of a template instance m 1 m 2 m. Let Λ(x : T 1 ).T be the type of the functor m 1 . Let T 2 be the type of the parameter m 2 . If the subtyping relation T 1 ≤ T 2 implies the proof obligation C then the type of

  in rule(2), the input clock e of the block stm; blk is passed to stm. The output clock e 1 of stm becomes the input clock of blk. The input and output clocks of an instruction may differ. This is the case, rule (3), for instruction if x then L 1 . Let e be the input clock of the instruction. If x is false then control is passed to the continuation of this instruction in the block, at the output clock e ∧ ¬x. Otherwise, control is passed to block L 1 , at the clock e ∧ x. Hence the type (e ∧ x) ⇒ L 2

	(2)	e

1 , E L : stm : P, e 2 e 2 , E L : blk : Q e 1 , E L : stm; blk : P | Q

URL: http://www.irisa.fr/espresso/Polychrony

CONFORMANCE CHECKING

Just as the multi-clocked synchronous formalism Signal it is based upon, our type system allows for the refinement-based design methodologies


Patrick Solé

Michel Planat

Robin inequality for 7-free integers

Keywords: Dedekind Ψ function, Robin inequality, Riemann Hypothesis, Primorial numbers

Recall that an integer is t-free iff it is not divisible by p t for some prime p. We give a method to check Robin inequality σ(n) < e γ n log log n, for t-free integers n and apply it for t = 6, 7. We introduce Ψ t , a generalization of Dedekind Ψ function defined for any integer t ≥ 2 by

If n is t-free then the sum of divisor function σ(n) is ≤ Ψ t (n). We characterize the champions for x → Ψ t (x)/x, as primorial numbers. Define the ratio R t (n) := Ψt(n) n log log n . We prove that, for all t, there exists an integer n 1 (t), such that we have R t (N n ) < e γ for n ≥ n 1 , where N n = n k=1 p k . Further, by combinatorial arguments, this can be extended to R t (N ) ≤ e γ for all N ≥ N n , such that n ≥ n 1 (t). This yields Robin inequality for t = 6, 7. For t varying slowly with N , we also derive R t (N ) < e γ .

I. INTRODUCTION

The Riemann Hypothesis (RH), which describes the non trivial zeroes of Riemann ζ function has been deemed the Holy Grail of Mathematics by several authors [START_REF] Borwein | The Riemann hypothesis. A resource for the afficionado and virtuoso alike[END_REF], [START_REF] Lachaud | L'hypothèse de Riemann : le Graal des mathématiciens[END_REF]. There exist many equivalent formulations in the literature [START_REF] Conrey | The Riemann hypothesis[END_REF]. The one of concern here is that of Robin [START_REF] Robin | Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann[END_REF], which is given in terms of σ(n) the sum of divisor function σ(n) < e γ n log log n, for n ≥ 5041. Recall that an integer is t-free iff it is not divisible by p t for some prime p. The above inequality was checked for many infinite families of integers in [START_REF] Choie | On Robin's criterion for the Riemann hypothesis[END_REF], for instance 5-free integers. In the present work we introduce a method to check the inequality for t-free integers for larger values of t and apply it to t = 6, 7. The idea of our method is to introduce the generalized Dedekind Ψ function defined for any integer t ≥ 2 by

Ψ t (n) := n p|n (1 + 1/p + • • • + 1/p t-1
).

If t = 2 this is just the classical Dedekind function which occurs in the theory of modular forms [START_REF] Csirik | On the genera of X0(N )[END_REF], in physics [START_REF] Planat | Riemann hypothesis from the Dedekind psi function[END_REF], and in analytic number theory [START_REF] Solé | Extreme values of the Dedekind Ψ function[END_REF]. By construction, if n is t-free then the sum of divisors function σ(n) is ≤ Ψ t (n). To see this note that the multiplicative function σ satisfies for any integer a in the range

t > a ≥ 2 σ(p a ) = 1 + p + • • • + p a ,
when the multiplicative function Ψ t satisfies

Ψ t (p a ) = p a + • • • + 1 + • • • + 1/p t-1-a .
It turns out that the structure of champion numbers for the arithmetic function x → Ψ t (x)/x is much easier to understand than that of x → σ(x)/x, the super abundant numbers. They are exactly the so-called primorial numbers (product of first consecutive primes). We prove that, in order to maximize the ratio R t it is enough to consider its value at primorial integers. Once this reduction is made, bounding above unconditionally R t is easy by using classical lemmas on partial eulerian products. We conclude the article by some results on t-free integers N ≥ N n , valid for t varying slowly with N. II. REDUCTION TO PRIMORIAL NUMBERS Define the primorial number N n of index n as the product of the first n primes

N n = n k=1 p k , so that N 0 = 1, N 1 = 2, N 2 = 6,
• • • and so on. The primorial numbers (OEIS sequence A002110 [11]) play the role here of superabundant numbers in [START_REF] Robin | Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann[END_REF] or primorials in [START_REF] Nicolas | Petites valeurs de la fonction d'Euler[END_REF]. They are champion numbers (ie left to right maxima) of the function x → Ψ t (x)/x :

Ψ t (m) m < Ψ t (n) n for any m < n. (1)
We give a rigorous proof of this fact. Proposition 1: The primorial numbers and their multiples are exactly the champion numbers of the function x → Ψ t (x)/x.

Proof: The proof is by induction on n. The induction hypothesis H n is that the statement is true up to N n . Sloane sequence A002110 begins 1, 2, 4, 6 . . . so that H 2 is true. Assume

H n true. Let N n ≤ m < N n+1 denote a generic integer. The prime divisors of m are ≤ p n . Therefore Ψ t (m)/m ≤ Ψ t (N n )/N n with equality iff m is a multiple of N n . Further Ψ t (N n )/N n < Ψ t (N n+1 )/N n+1 . The proof of H n+1 follows.
In this section we reduce the maximization of R t (n) over all integers n to the maximization over primorials.

Proposition 2: Let n be an integer ≥ 2. For any m in the range

N n ≤ m < N n+1 one has R t (m) < R t (N n ).
Proof: Like in the preceding proof we have

Ψ t (m)/m ≤ Ψ t (N n )/N n .
Since 0 < log log N n ≤ log log m, the result follows.

III. Ψ t AT PRIMORIAL NUMBERS We begin by an easy application of Mertens formula. Proposition 3: For n going to ∞ we have

lim R t (N n ) = e γ ζ(

t) .

Proof:

Writing 1 + 1/p = (1 -1/p 2 )/(1 -1/p) in the definition of Ψ(n) we can combine the Eulerian product for ζ(t) with Mertens formula p≤x (1 -1/p) -1 ∼ e γ log(x) to obtain Ψ(N n ) ∼ e γ ζ(t) log(p n ).
Now the Prime Number Theorem [6, Th. 6, Th. 420] shows that x ∼ θ(x) for x large, where θ(x) stands for Chebyshev's first summatory function:

θ(x) = p≤x log p.
This shows that, taking x = p n we have

p n ∼ θ(p n ) = log(N n ).
The result follows. This motivates the search for explicit upper bounds on R t (N n ) of the form e γ ζ(t) (1 + o(1)). In that direction we have the following bound.

Proposition 4: For n large enough to have p n ≥ 20000, we have

Ψ t (N n ) N n ≤ exp(γ + 2/p n ) ζ(t) (log log N n + 1.1253 log p n ).
We prepare for the proof of the preceding Proposition by some Lemmas. First an upper bound on a partial Eulerian product from [13, (3.30) ).

On taking log's we obtain log log N n > log p n -0.1253 p n ,

upon using log(1 - x 8 ) > -0.1253x
for x small enough. In particular x < 1/20000 is enough.

We are now ready for the proof of Proposition 4.

Proof:

Write Ψ t (N n ) N n = n k=1 1 -1/p k t 1 -1/p k = p>pn (1 -1/p t ) -1 ζ(t) p≤pn (1 -1/p) -1
and use both Lemmas to derive

Ψ t (N n ) N n ≤ exp(γ + 2/p n ) ζ(t) (log p n + 1 log p n ).
Now we get rid of the first log in the RHS by Lemma 3.

The result follows.

So, armed with this powerful tool, we derive the following significant Corollaries. For convenience let

f (n) = (1 + 1.1253 log p n log log N n ).
Corollary 1:

Let n 0 = 2263. Let n 1 (t) denote the least n ≥ n 0 such that e 2/pn f (n) < ζ(t). For n ≥ n 1 (t) we have R t (N n ) < e γ .
Proof:

Let n ≥ n 0 . We need to check that exp(2/p n )(1 + 1.1253 log p n log log N n ) ≤ ζ(t).
which, for fixed t holds for n large enough. Indeed ζ(t) > 1 and the LHS goes monotonically to 1 + for n large.

We give a numerical illustration of Corollary 1 in Table 1. We can extend this Corollary to all integers ≥ n 0 by using the reduction of preceding section. Corollary 2: For all N ≥ N n such that n ≥ n 1 (t) we have R t (N) < e γ .

t
Proof: Combine Corollary 1 with Proposition 2. We are now in a position to derive the main result of this note. Theorem 1: If N is a 7-free integer, then σ(N) < Ne γ log log N.

Proof: If N is ≥ N n with n ≥ n 1 (7), then the above upper bound holds for Ψ 7 (N) by Corollary 2, hence for σ(N) by the remark in the Introduction. If not, we invoke the results of [START_REF] Briggs | Abundant numbers and the Riemann hypothesis[END_REF], who checked Robin inequality for 5040 < N ≤ 10 10 10 , and observe that all 7-free integers are > 5040.

IV. VARYING t

We begin with an easy Lemma. Lemma 4: Let t be a real variable. For t large, we have

ζ(t) = 1 + 1 2 t + o( 1 2 t
). Proof: By definition, for t > 1 we may write

ζ(t) = ∞ n=1 1 n t so that ζ(t) ≥ 1 + 1 2 t .
In the other direction, we write

ζ(t) = 1 + 1 2 t + 1 3 t + ∞ n=4 1 n t ,
and compare the remainder of the series expansion of the ζ function with an integral:

∞ n=4 1 n t < ∞ 3 du u t = 3 (t -1)3 t = O( 1 3 t ).
The result follows.

We can derive a result when t grows slowly with n. Theorem 2: Let S n be a sequence of integers such that S n ≥ N n for n large, and such that S n is t-free with t = o(log log n). For n large enough, Robin inequality holds for S n .

Proof: For Corollary 2 to hold we need

e 2/pn f (n) < ζ(t)
to hold, or , taking logs, the exact bound

2/p n + log f (n) < log ζ(t),
or up to o(1) terms

2/p n + 1.1253 log p n log log N n ≤ log ζ(t).
In the LHS, the dominant term is of order 1/(log p n ) 2 , since, like in the proof of Proposition 3, we may write p n ∼ log N n . Now p n ∼ n log n by [6, Th. 8], entailing log p n ∼ log n and (log p n ) 2 ∼ (log n) 2 . In the RHS, with the hypothesis made on t we have, by Lemma 4, the estimate log ζ(t) ∼ 1 2 t . The result follows after comparing logarithms of both sides.

V. CONCLUSION

In this article we have proposed a technique to check Robin inequality for t-free integers for some values of t. The main idea has been to investigate the complex structure of the divisor function σ though the sequence of Dedekind psi functions ψ t . The latter are simpler for the following reasons

• Ψ t (n) solely depends on the prime divisors of n and not on their multiplicity • the champions of Ψ t are the primorials instead of the colossally abundant numbers • Ψ t is easier to bound for n large because of connections with Eulerian products Further, σ(n) ≤ Ψ t (n) for t-free integers n. We checked Robin inequality for t-free integers for t = 6, 7 and t = o(log log n). It is an interesting and difficult open problem to apply Theorem 2 to superabundant numbers or colossally abundant numbers for instance. We do not believe it is possible. New ideas are required to prove Robin inequality in full generality.

  p.70]. Lemma 1: For x ≥ 2, we have

	p≤x	(1 -1/p) -1 ≤ e γ (log x +	1 log x	).
		log p n < log log N n +	0.1253 log p n	.

Next an upper bound on the tail of the Eulerian product for ζ(t).

Lemma 2: For n ≥ 2 we have

p>pn (1 -1/p t ) -1 ≤ exp(2/p n ).

Proof: Use Lemma 6.4 in

[START_REF] Choie | On Robin's criterion for the Riemann hypothesis[END_REF]

with x = p n . Bound t t-1 x 1-t above by 2/x. Lemma 3: For n ≥ 2263, we have Proof: If n ≥ 2263, then p n ≥ 20000. By [13], we know then that log N n > p n (1 -1 8p n

TABLE I :

 I The numbers in Corollary 1.

		n 1 (t)	N n1(t)
	3	10	6.5 × 10 9
	4	24	2.4 × 10 34
	5	79	4.1 × 10 163
	6	509	5.8 × 10 1551
	7 10 596 2.5 × 10 48337