Eugene Yip
email: eugene.yip@uni-bamberg.de

Alain Girault
email: alain.girault@inria.fr

Partha S Roop
email: p.roop@auckland.ac.nz

Morteza Biglari-Abhari

The ForeC Synchronous Deterministic Parallel Programming Language for Multicores (Invited Paper)

Cyber-physical systems (CPSs) are embedded systems that are tightly integrated with their physical environment. The correctness of a CPS depends on the output of its computations and on the timeliness of completing the computations. This paper proposes the ForeC language for the deterministic parallel programming of CPS applications on multi-core execution platforms. ForeC's synchronous semantics is designed to greatly simplify the understanding and debugging of parallel programs. ForeC allows programmers to express many forms of parallel patterns while ensuring that programs are amenable to static timing analysis. One of ForeC's main innovation is its shared variable semantics that provides thread isolation and deterministic thread communication. Through benchmarking, we demonstrate that ForeC can achieve better parallel performance than Esterel, a widely used synchronous language for concurrent safetycritical systems, and OpenMP, a popular desktop solution for parallel programming. We demonstrate that the worst-case execution time of ForeC programs can be estimated precisely.

Introduction

Safety-critical embedded systems must be dependable and functionally safe [START_REF] Paolieri | Towards Functional-Safe Timing-Dependable Real-Time Architectures[END_REF] and certified against safety standards, such as DO-178B [START_REF]Software Considerations in Airborne Systems and Equipment Certification[END_REF]. Certification is a costly and time consuming exercise and is exacerbated by the use of multi-core processors. The correctness of a safety-critical embedded systems depends on the output of its computations and on the timeliness of completing the computations [START_REF] Wilhelm | Computation Takes Time, but How Much?[END_REF] in response to inputs. Thus, a key to building successful embedded systems using multi-cores is the understanding of the timing behaviors of the computations [START_REF] Axer | Building Timing Predictable Embedded Systems[END_REF]. This is typically achieved with static worst-case execution time (WCET) analysis [START_REF] Wilhelm | The Worst-Case Execution-Time Problem -Overview of Methods and Survey of Tools[END_REF] and is a complex process because it depends on the underlying execution platform.

C [6] is a popular language for programming embedded systems with support for multi-threading and parallelism provided by third-party libraries, such as Pthreads [START_REF]The IEEE and The Open Group[END_REF] and OpenMP [START_REF]OpenMP Application Program Interface[END_REF]. Unfortunately, these multi-threading solutions are inherently non-deterministic [START_REF] Lee | The Problem with Threads[END_REF] and programmers fall into common parallel programming traps and pitfalls [START_REF] Lu | Learning from Mistakes: A Comprehensive Study on Real World Concurrency Bug Characteristics[END_REF]. To help alleviate this issue, runtime environments that enforce deterministic thread scheduling and memory accesses can be used. CoreDet [START_REF] Bergan | CoreDet: A Compiler and Runtime System for Deterministic Multithreaded Execution[END_REF] maps all thread interactions onto a logical timeline. The program's execution alternates between parallel and serial phases. However, understanding the program's behavior at compile time remains difficult because the determinism is enforced by the runtime. Threads in CoreDet maintain their own snapshot of the shared memory state, which is resynchronized in every serial phase. This concept is used and formally defined in Concurrent revisions [START_REF] Burckhardt | Semantics of Concurrent Revisions[END_REF]. An alternative is to extend the C language with deterministic parallelism, such as SharC [START_REF] Raman | Efficient Data Race Detection for Async-Finish Parallelism[END_REF], but its time predictability is unknown.

Synchronous languages [START_REF] Benveniste | The Synchronous Languages 12 Years Later[END_REF], such as Esterel [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics and Implementation[END_REF], provide an alternative by offering deterministic concurrency that is based on sound mathematical semantics, which facilitates system verification by formal methods [START_REF] Souyris | Computing the Worst Case Execution Time of an Avionics Program by Abstract Interpretation[END_REF]. Figure 1 depicts a synchronous program, defined as a set of concurrent threads, within its physical environment. A synchronous program reacts to inputs by producing corresponding outputs. Each reaction is triggered by a hypothetical (logical) global clock. Central to synchronous languages is the synchrony hypothesis [START_REF] Benveniste | The Synchronous Languages 12 Years Later[END_REF], which states that the execution of each reaction is considered to be atomic and instantaneous. Concurrent threads communicate instantaneously with each other (dashed arrows in Figure 1) using signals. Once the embedded system is implemented, the synchrony hypothesis is validated by ensuring that the WCET of any global tick does not exceed the minimal inter-arrival time of the inputs. This is known as worst-case reaction time analysis and techniques have been developed for multi-cores [START_REF] Ju | Timing Analysis of Esterel Programs on General-Purpose Multiprocessors[END_REF], [START_REF] Yip | Programming and Timing Analysis of Parallel Programs on Multicores[END_REF]. C-based synchronous languages, such as PRET-C [START_REF] Andalam | Predictable Framework for Safety-Critical Embedded Systems[END_REF] and SyncCharts in C [START_REF] Hanxleden | SyncCharts in C -A Proposal for Light-Weight, Deterministic Concurrency[END_REF], appeal to C programmers because the learning barrier for synchronous languages is reduced. However, their inherent sequential execution semantics render them unsuitable for multi-core execution.

Synchronous programs are considerably difficult to parallelize [START_REF] Girault | A Survey of Automatic Distribution Method for Synchronous Programs[END_REF] due to the need to resolve instantaneous thread communication and associated causality issues. At runtime, all potential signal emitters must be executed before all testers of a signal. If this is not possible, then a causality issue arises. Hence, concurrency is typically compiled away to produce only sequential code [START_REF] Edwards | Code Generation in the Columbia Esterel Compiler[END_REF] that is then parallelized [START_REF] Girault | A Survey of Automatic Distribution Method for Synchronous Programs[END_REF], [START_REF] Baudisch | Multithreaded Code from Synchronous Programs: Extracting Independent Threads for OpenMP[END_REF]. The Synchronized Distributed Executive (SynDEx) [START_REF] Potop-Butucaru | Semantics-Preserving Implementation of Synchronous Specifications Over Dynamic TDMA Distributed Architectures[END_REF] approach considers communication costs when distributing code to each processing element. Yuan et al. [START_REF] Yuan | Architectures Specific Compilation for Efficient Execution of Esterel[END_REF] offer static and dynamic scheduling approaches for Esterel on multi-cores.

Contributions. The synchronous languages designed for the single-core era must be redesigned to address the multi-core challenges. Section 2 describes the multi-core architecture considered by this paper. We propose a C-based synchronous parallel programming language, called ForeC, for simplifying the deterministic parallel programming of embedded multi-cores. ForeC brings together the formal deterministic semantics of synchronous languages and the benefits of C's control and data structures (Section 3). A key innovation is ForeC's shared variable semantics that provides thread isolation and deterministic thread communication. Moreover, many forms of parallel programming patterns can be expressed in ForeC, such as the software pipeline design pattern in Section 4. ForeC can be compiled for direct execution on embedded multi-cores or for execution on desktop multi-cores using an operating system (Section 5). Through benchmarking in Section 6, we demonstrate that ForeC can achieve better parallel performance than Esterel and OpenMP, while being amenable to static timing analysis. Section 7 concludes the paper.

Multi-Core Architecture

The architecture of the predictable multi-core used in this paper is representative of existing predictable designs [START_REF] Cullmann | Predictability Considerations in the Design of Multi-Core Embedded Systems[END_REF]. It is a homogeneous multi-core processor that we have designed using Xilinx MicroBlaze [START_REF] Xilinx | MicroBlaze Processor Reference Guide[END_REF] cores. Each MicroBlaze core has a three-stage in-order pipeline that is free of timing anomalies and is connected to private data and instruction scratchpads. The scratchpads are statically allocated and loaded at compile time. A shared bus with TDMA arbitration connects the cores to shared resources, such as global memory and peripherals. We developed a multi-core MicroBlaze simulator for benchmarking purposes by extending an existing MicroBlaze simulator [START_REF] Whitham | Scratchpad Memory Management Unit[END_REF] to support cycle-accurate simulation, an arbitrary number of cores, and a shared bus with TDMA arbitration. We observe that the focus of the paper is not on architectural innovations for time predictability, but rather language theoretic innovations (Section 3).

The ForeC Language

ForeC inherits the benefits of synchrony, such as determinism and reactivity, along with the benefits and power of the C language, such as control and data structures. This is unlike conventional synchronous languages, which treat C as an external host language. A key goal of ForeC is in providing deterministic shared variable semantics that is agnostic to scheduling. This is essential for the reasoning and debugging of parallel programs.

Overview of ForeC

ForeC extends a safety-critical subset of C [START_REF] Blazy | Mechanized Semantics for the Clight Subset of the C Language[END_REF] with a minimal set of synchronous constructs. Although C [6] is popular for programming safety-critical embedded systems, it has unspecified and undefined behaviors. Safety-critical programmers follow strict coding guidelines [START_REF]MISRA-C: 2012: Guidelines for the Use of the C Language in Critical Systems[END_REF] to help write deterministic programs that are understandable, maintainable, and easier to debug. We describe the statements, specifiers, and qualifiers allowed in the C subset:

C statements (c st): Expressions can only be constants, variables, pointers, and array elements that are composed with the logical, bitwise, relational, and arithmetic operators of C. Although the use of pointers and arrays is allowed, pointer aliasing makes static analysis difficult [START_REF] Buss | A Novel Analysis Space for Pointer Analysis and Its Application for Bug Finding[END_REF]. Thus, we assume that pointers are only assigned once. All C control statements, except goto, can be used.

C type specifiers and qualifiers: All the C primitives and qualifiers can be used. Custom data types can be defined using struct, union, and enum.

C storage class specifiers: The C typedef, extern, static, auto, and register specifiers can be used.

Figure 2 gives the extended syntax of ForeC and Table 1 summarizes the informal semantics. A statement (st) in ForeC can be a traditional C statement (c st), or a barrier (pause), fork/join (par), or preemption (abort) statement. Using the sequence operator ( ; ) a statement in ForeC can be an arbitrary composition of other statements. Like C, extra properties can be specified for variables using type qualifiers. A type qualifier (tq) in ForeC is a traditional C type qualifier (c tq), an environment interface (input and output), or a shared variable amongst threads (shared). input: Type qualifier to declare an input, the value of which is updated by the environment at the start of every global tick. output: Type qualifier to declare an output, the value of which is emitted to the environment at the end of every global tick. shared: Type qualifier to declare a shared variable, which can be accessed by multiple threads. pause: Pauses the executing thread until the next global tick. par(st, st): Forks two statements st as parallel threads. The par terminates when both threads terminate (join back). weak? abort st when immediate? (exp): Preempts its body st when the expression exp evaluates to a non-zero value. The optional weak and immediate keywords modify its temporal behavior.

and emit their results to the environment. When a thread completes its computation, we say that it completes its local tick. When all threads complete their local ticks, we say that the program completes its global tick. The program below declares two input and two output variables, and a main thread that forks the execution of two threads that each have three sequential statements:

i n p u t i n t X, Y ; o u t p u t i n t A=0 , B= 0 ; v o i d main ( v o i d ) { par ( t 1 ( ) , t 2 ( ) ) ; } v o i d t 1 ( v o i d ) { i n t a = 1+X ; pause ; A = a * X ; } v o i d t 2 ( v o i d ) { i n t b = 1+Y ; pause ; B = b * Y ; }
Inputs are read-only and their values are updated by the environment at the start of each global tick. Outputs emit their values to the environment at the end of each global tick. The program starts its first global tick from the main thread. The main thread executes the par statement that forks its arguments (the functions t1 and t2) into two parallel child threads. The par is a blocking statement and terminates only when both its child threads terminate, i.e., join together. The child threads t1 and t2 initialize their local variables by incrementing the input values by 1. Let the values of the inputs be X=1 and Y=2 during the first global tick. Hence, thread t1 assigns a=2 and thread t2 assigns b=3. Both child threads execute a pause statement, which pauses their execution and acts as a synchronization barrier. We say that both threads have completed their local ticks. Next, the program completes its first global tick and the outputs A=0 and B=0 are emitted.

The program starts its second global tick by resuming the child threads t1 and t2 from their respective pause statements. That is, both threads begin their next local ticks. Let the values of the inputs be X=3 and Y=4 during the second global tick. Thread t1 assigns A=6 and thread t2 assigns B=12 to the output variables. Both child threads terminate, causing the par statement in the main thread to terminate. The main thread resumes its execution by reaching the end of its body and terminating. The second global tick ends and the outputs A=6 and B=12 are emitted.

3.1.2. Shared Variables. All variables in ForeC follow the scoping rules of C. By default, all variables are private and can only be accessed (read or write) by one thread throughout its scope. To allow a variable to be accessed by multiple threads, it must be declared as a shared variable by using the shared type qualifier. Thus, any misuse of private variables are easy to detect at compile time. The semantics for shared variables permit them to be accessed deterministically in parallel, without needing the programmer to explicitly use mutual exclusion. We modify our program by making the child threads t1 and t2 share the variable x:

i n p u t i n t X, Y; o u t p u t i n t A= 0 ; v o i d main ( v o i d ) {
s h a r e d i n t x=1 combine a l l w i t h p l u s ;

par ( t 1 (&x ) , t 2 (&x ) ) ; A = x ; } v o i d t 1 ( s h a r e d i n t * x ) { x = 1+X; pause ; x = x * X; } v o i d t 2 ( s h a r e d i n t * x ) { x = 1+Y; pause ; x = x * Y; } i n t p l u s ( i n t t h 1 , i n t t h 2 ) { r e t u

r n ( t h 1 + t h 2 ) ; }

The main thread now declares a shared variable called x. C's call by reference is used to pass x to the child threads. When the child threads start their local tick, they each create a local copy of x. When the child threads need to access x, they access their copy of x instead. Hence, their copies of x remain distinct from the shared variable x declared in the main thread. The changes made by one thread cannot be observed by any other, yielding mutual exclusion and thread isolation. Thread isolation minimizes the need to serialize parallel accesses to shared variables, thereby maximizing runtime parallelism. This is key to enhancing execution performance and is unlike conventional synchronousreactive languages [START_REF] Girault | A Survey of Automatic Distribution Method for Synchronous Programs[END_REF]. Moreover, only sequential reasoning is needed within the thread's local tick. Next, let the values of the inputs be X=1 and Y=2 during the first global tick. Threads t1 and t2 assign 2 and 3, respectively, to their local copies of x before pausing. The first global tick ends and the local copies of x are automatically combined into a single value by a programmer-specified combine function. The combine function for the shared variable x is plus, specified in the combine clause of its declaration. Thus, the combined value of both copies is plus(2,3)=5 and is assigned to the shared variable x. We call the combined value that is assigned to the shared variable the resynchronized value and call the process of updating the shared variable as resynchronizing. Resynchronizing shared variables at the end of each global tick ensures deterministic outputs at the

= || | && | ˆ| | | & | << | >> | == | != | < | > | <= | >= | + | -| * | / | % Figure 3. Syntax of preemption conditions.
end of each global tick. Finally, the first global tick ends and the output A=0 is emitted.

When the program starts its second global tick, the child threads start their next local ticks by creating a local copy of x. Their copies are initialized with x's resynchronized value of 5. Let the values of the inputs be X=3 and Y=4 during the second global tick. Threads t1 and t2 assign 15 and 20, respectively, to their local copies of x and terminate. When all the child threads of a par terminate, their local copies are automatically combined and assigned to their parent thread. In this case, the combined value of both copies is plus(15,20)=35. The main thread resumes and assigns the combined value of x to the output A and then terminates. The second global ends and the output A=35 is emitted.

Combine Functions and Policies. The signature of any combine function is

C : Val × Val → Val .
The two input parameters are the two copies to be combined. A combine function is invoked multiple times when more than two copies need to be combined, e.g.,

c(v 1 , c(v 2 , • • • c(v n-1 , v n )))).
Combine functions must be deterministic, associative, and commutative. That is, they produce the same outputs from the same inputs, regardless of previous invocations and how the copies are ordered or grouped. ForeC's combine functions are inspired by Esterel [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics and Implementation[END_REF] but similar solutions can be found in other parallel programming frameworks, e.g., OpenMP's reduction operators [START_REF]OpenMP Application Program Interface[END_REF]. Solutions developed for these frameworks could be reworked into ForeC combine functions and policies.

It may be useful to ignore some of the copies when resynchronizing a shared variable. This is achieved by specifying a combine policy that determines what copies will be ignored. The combine policies are new, mod, and all and they are used in the combine clause during variable declaration, e.g., combine new with. The new policy ignores the copies that have the same value as their shared variable's resynchronized value. The mod policy ignores the copies that were not assigned a value during the global tick. The default policy is all where no copies are ignored. Note that the combine function is not invoked when only one copy remains. Instead, that copy is resynchronized value. [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics and Implementation[END_REF], the abort st when (exp) statement provides preemption, which is the termination of the abort body st when the condition exp evaluates to true. Preemption can be used to model hierarchical state machines succinctly. The condition exp must be a side-effect free expression produced from the syntax shown in Figure 3. The program below is an example of a non-immediate and strong abort:

Preemption. Inspired by Esterel

v o i d main ( v o i d ) { i n t x = 1 ;
a b o r t { x = 2 ; pause ; x = 3 ; pause ; x = 4 ; } when ( x >2) ; } After initializing variable x to 1, execution reaches the abort. x=2 is executed and then the first global tick ends. At the start of the second global tick (and at each subsequent global tick), the preemption condition is evaluated before the abort body can execute. This allows shared variables in the condition to be evaluated with their resynchronized value. If the preemption condition evaluates to true (any non-zero value following the C convention), then the abort terminates without executing its body. For this abort example, the preemption condition is true at the start of the third global tick, as x=3. An abort will also terminate when execution reaches the end of its body.

Like Esterel, the optional weak and immediate keywords change the temporal behavior of the preemptions. The weak keyword delays the termination of the abort body until the body cannot execute any further, e.g., reaches a pause statement. The following is an example of a nonimmediate and weak abort:

v o i d main ( v o i d ) { i n t x = 1 ;
weak a b o r t { x = 2 ; pause ; x = 3 ; pause ; x = 4 ; pause ; } when ( x >2) ; } Here, although the preemption condition is true at the start of the third global tick, the termination of the abort is delayed until the third pause is reached.

The immediate keyword allows the abort to terminate immediately as soon as execution reaches it for the first time. The following is an example of an immediate and strong abort:

v o i d main ( v o i d ) { i n t x = 3 ; a b o r t {
x = 2 ; pause ; x = 3 ; pause ; x = 4 ; } when immediate ( x >2) ; } Here, the initial value of x is 3, meaning that the preemption condition is true when execution first reaches the abort. Hence, the abort body is not executed at all.

Lastly, both the weak and immediate keywords can be used together to define an immediate and weak abort:

v o i d main ( v o i d ) { i n t x = 3 ;
weak a b o r t { x = 2 ; pause ; x = 3 ; pause ; x = 4 ; } when immediate ( x >2) ; } Here, the preemption condition is true when execution first reaches the abort. However, the termination of the abort is delayed until the first pause is reached.

Comparison with Esterel and Concurrent Revisions

This section compares ForeC with Esterel [START_REF] Berry | The Esterel Synchronous Programming Language: Design, Semantics and Implementation[END_REF] and Concurrent revisions [START_REF] Burckhardt | Semantics of Concurrent Revisions[END_REF]. Concurrent revisions is a programming model that supports the forking and joining of asynchronous threads. When a thread is forked, it creates a snapshot of the shared variables. Changes performed by the thread are applied to its snapshot, thus, ensuring thread isolation. The snapshots are merged together using a deterministic merge function when the threads join. The merge function always considers all the copies, i.e., equivalent to ForeC's combine policy all. Thread communication is, therefore, always delayed until the child threads join. In contrast, ForeC threads may execute over several global ticks and thread communication is only delayed to the end of each global tick. Esterel threads communicate instantaneously by emitting and receiving signals during each global tick. Signal emissions may have associated values that must be combined using a programmer-specified combine function before the signal can be read. Esterel's combine function only considers the emitted values, i.e., equivalent to ForeC's combine policy mod.

In Concurrent revisions, the parent thread can execute alongside its children and, e.g., fork more threads in response to higher input workloads. This is not the case with ForeC and Esterel because the parent thread blocks until of all its children have joined. The commutativity and associativity of ForeC, Esterel, and Concurrent revisions' parallel construct depends on the commutativity and associativity of their combine and merge functions, respectively.

Preemptions in Esterel are triggered instantaneously by instantaneous signal communication. However, preemptions in ForeC are triggered after a delay of one global tick because preemption conditions are evaluated using values computed in the previous global tick. Concurrent revisions does not support preemptions. Esterel programs may be non-causal [START_REF] Benveniste | The Synchronous Languages 12 Years Later[END_REF] because of instantaneous feedback cycles. Thanks to delayed communication, programs in ForeC and Concurrent revisions are always causal by construction.

Software Pipeline Design Pattern in ForeC

Design patterns [START_REF] Mccool | Structured Parallel Programming[END_REF] are reusable templates that programmers can use to solve recurring problems of any size and achieve high execution performance. For example, the software pipeline pattern [START_REF] Mccool | Structured Parallel Programming[END_REF] solves the problem of needing to process an audio or video data stream in stages. An instance of this pattern in ForeC is given in Figure 4. The data processing is broken down into pipeline stages that work in parallel on different chunks of the data stream. The pattern forks a thread for each pipeline stage. Each stage gets a chunk of data, processes the data, and passes the result to i n p u t i n t i n ; o u t p u t i n t o u t ; s h a r e d i n t s 1 =0 , s 2 = 0 ;

v o i d main ( v o i d ) {
par ( s t a g e 1 ( ) , par ( s t a g e 2 ( ) , s t a g e 3 ( ) ) ) ; the next stage. This is repeated until the data stream ends. Data is passed from each stage using shared variables.

} v o i d s t a g e 1 ( v o i d ) { w h i l e (
The explicit use of buffers is not needed because threads always work on local copies of the shared variables. The pipeline is synchronous because the stages pause before processing their next chunk of data. Hence, the throughput is determined by the slowest pipeline stage. To initialize the pipeline correctly, each stage must wait for their initial chunk of data. The waiting is achieved by placing, at the start of the threads, a number of pause statements equal to the number of preceding stages. The stages execute in parallel after all have waited for their initial chunk of data.

Compiling ForeC for Parallel Execution

The ForeC compiler generates statically scheduled code for direct execution on a predictable parallel architecture described in Section 2. The aim is to generate performant code that is amenable to static timing analysis. The compiler translates the ForeC statements into equivalent C code and generates thread scheduling routines for each core. The programmer statically allocates the threads to the cores and passes the allocations into the compiler. Based on the allocations, the compiler defines a total order for all the threads, using on a depth-first traversal of the program's control-flow graph. A static and non-preemptive (cooperative) schedule is created for each core, encoded as a doubly linked list, similar to the approach of the Columbia Esterel Compiler [START_REF] Edwards | Code Generation in the Columbia Esterel Compiler[END_REF]. Each thread is represented as a node in the linked list of its allocated core. The node stores the thread's continuation point (a program counter) and links to the threads (nodes) that are scheduled before and after it. The initial continuation point of a thread is the start of its body. Each core begins its execution by jumping to the continuation point of the first thread in its linked list. The thread executes without interruption until it reaches a context-switching point: a par or pause statement, or the end of its body. At this point, the thread stores its next continuation point into its node and jumps to the continuation point in the next node. Thus, inserting or removing a thread or routine from the list controls whether it is included or excluded, respectively, from execution.

A problem with encoding the static schedule as a linked list is that the global tick in which threads fork and join can only be determined at runtime. This means that threads need to be inserted or removed from the linked lists whenever they are forked or whenever they terminate. This is managed by inserting synchronization routines into the linked lists that send and receive scheduling information between cores at runtime. For example, when a parent thread on one core reaches a par, the other cores receive this information via their synchronization routines and will insert the newly forked threads into their linked lists. The notion of a global tick is preserved by ending each linked list with a global tick synchronization routine that implements barrier synchronization. One core is nominated to perform the following housekeeping tasks: resynchronizing the shared variables, emitting the outputs, and sampling the inputs.

Shared variables are hoisted up to the program's global scope to allow all cores to access them. The copies of shared variables are implemented as unique global variables. In each thread, all shared variable accesses are replaced by accesses to their copies.

Benchmarks

This section begins by evaluating the static worst-case reaction time (WCRT) analysis of ForeC programs. We have previously shown [START_REF] Yip | Programming and Timing Analysis of Parallel Programs on Multicores[END_REF] that the WCRT of ForeC programs could be estimated to a high degree of precision, which is very useful for implementing real-time embedded systems. Further, we provide a performance comparison between ForeC and Esterel. Although ForeC has been designed with embedded multi-cores in mind, we believe that the ForeC language can be applied to the deterministic parallel programming of desktop multi-cores. Performant parallel programs can be achieved by using parallel design patterns within a synchronous language, like ForeC. We evaluate this hypothesis with a performance comparison to OpenMP, a popular desktop solution for parallel programming that primarily exploits loop data parallelism.

Time Predictability

ForeC is amenable to static timing analysis because we implement all language features using static scheduling. Additionally, bounded loops are used to ensure bounded execution times, synchronous preemption is used instead of (asynchronous) hardware interrupts, and threads execute in isolation thanks to the shared variable semantics. Our C++ ForeCast tool [START_REF] Yip | Programming and Timing Analysis of Parallel Programs on Multicores[END_REF] statically analyzes the WCRT of ForeC programs on embedded multi-cores. This section highlights our key findings [START_REF] Yip | Programming and Timing Analysis of Parallel Programs on Multicores[END_REF] for the MicroBlaze multi-core simulator described in Section 2, with the configuration shown in Figure 5. The 802.11a [START_REF] Pop | A Stream-Computing Extension to OpenMP[END_REF] benchmark is production code from Nokia, that tests various signal processing algorithms needed to decode 802.11a data transmissions. 802.11a has complex data and control dominated computations, comprised of 2147 lines of ForeC code that forks 26 threads, of which up to 10 can execute in parallel. 802.11a was Xilinx MicroBlaze, 3-stage pipeline, no branch prediction, no caches, no out-of-order execution, 8 KB private data and instruction scratchpads on each core (1 cycle access time), 32 KB global memory (5 cycle access time), TDMA shared bus (5 cycle time slots per core and, thus, a 5×(number of cores) cycle long bus schedule), programs compiled with MB-GCC-4.1.2 -O0 and decompiled with MB-OBJDUMP-4.1.2. distributed on up to 10 cores and ForeCast computed the WCRT of each distribution. To evaluate the precision of the computed WCRTs, 802.11a was executed by the multicore simulator for one million reactions unless the program terminated. Test vectors were generated to elicit the worstcase execution path by studying the program's control-flow. The simulator reported the execution time of each global tick and the longest was taken as the observed WCRT. The observed and computed WCRTs of 802.11a are plotted as a line graph in Figure 6. This graph shows that Fore-Cast is very precise, even as the number of cores increased. ForeCast computed WCRTs that were only 3.2% longer than the observed WCRTs. Similar levels of precision have been demonstrated with other benchmark programs [START_REF] Yip | Programming and Timing Analysis of Parallel Programs on Multicores[END_REF]. The computed WCRTs of 802.11a in Figure 6 also reflect the benefit of multi-core execution. The computed WCRT decreased when the number of cores increased from one to five. The computed WCRT at five cores corresponded to the execution time of one thread that was already allocated to its own core. Thus, the WCRT could not be improved by distributing the remaining threads. The WCRT increased after five cores because of increased scheduling overheads and global memory access times. Ju et al. [START_REF] Ju | Timing Analysis of Esterel Programs on General-Purpose Multiprocessors[END_REF] offer the only other known static WCRT analysis approach for synchronous programs on multi-cores. Unfortunately, we cannot compare with that work because their results are only for a four core system with no precision results reported.

Comparison with Esterel

The dynamic scheduling approach by Yuan et al. [START_REF] Yuan | Architectures Specific Compilation for Efficient Execution of Esterel[END_REF] for Esterel programs has been shown to perform well on a

Comparison with OpenMP

We extended the ForeC compiler to target desktop multicores running an operating system. For each core, the compiler creates a Pthread [START_REF]The IEEE and The Open Group[END_REF] to run its static thread schedule. Hence, a fixed pool of Pthreads executes the ForeC threads, so the cost of creating each Pthread is only incurred once. Although the Pthreads are dynamically scheduled by the operating system, the original ForeC threads follow their Single-threaded C, ForeC, and OpenMP versions of each benchmark program were created and handcrafted for best performance. For the ForeC versions, FmRadio used the software pipeline and fork-join patterns and Lzss used the fork-join pattern. The Intel VTune Amplifier XE [START_REF] Intel | Intel R VTune TM Amplifier[END_REF] software helped identify areas of code that could be parallelized for the OpenMP versions of the benchmarks. Benchmarking was carried out on a 3.4 Ghz four-core Intel Core-i5 3570 desktop running Linux 3.6 with 8 GB of RAM. Hyper-Threading, Turbo Boost, and SpeedStep were disabled. The benchmarks were compiled with GCC-4.8 -O2.

Table 3 shows the average speedups achieved by ForeC and OpenMP. Speedups were calculated using equation [START_REF] Paolieri | Towards Functional-Safe Timing-Dependable Real-Time Architectures[END_REF]. Although ForeC and OpenMP achieved a speedup of between two and four, ForeC demonstrates greater speedup than OpenMP in these preliminary results. Dynamic and static thread scheduling pragmas were used in the OpenMP versions and dynamic scheduling does introduce slight overheads, especially thread locking, but these overheads should be amortized over the overall run of the benchmarks. This scheduling approach of OpenMP contrasts with the ForeC approach, where all work scheduling is static and determined automatically by the ForeC compiler.

Conclusions

This paper introduced the ForeC language that enables the deterministic parallel programming of multi-cores. The language features of ForeC help bridge the differences between synchronous-reactive programming and generalpurpose parallel programming. The local copying of shared variables ensures thread isolation and determinism, while minimizing the need to serialize parallel accesses to shared variables. The behavior of shared variables can be tailored to the application at hand by specifying suitable combine functions and policies. A critical comparison showed that ForeC combines the benefits offered by synchronous languages with those offered by deterministic runtime solutions. To the best of our knowledge, no other synchronous language achieves parallel execution and time predictability similar to ForeC. For future work, the ForeC compiler could be improved to generate more efficient code that remains amenable to static timing analysis. In particular, different static scheduling strategies could be explored for different parallel programming patterns. The allocation of ForeC threads could be refined automatically by feeding ForeCast's WCRT analysis results back into the ForeC compiler.

Figure 1 .

 1 Figure 1. Synchronous model of computation.

3. 1 . 1 .

 11 I/O, Threads, and Pausing. Like traditional C programs, the function main is the program's entry point and serves as the initial thread of execution. To recap, the threads of a synchronous program execute in lock-step to the ticking of a global clock. During each global tick, the threads sample the environment, perform their computations, Statements: st ::= c st | pause | par(st, st) | weak? abort st when immediate? (exp) | st; st Type Qualifiers: tq ::= c tq | input | output | shared

Figure 2 .

 2 Figure 2. Syntactic extensions to C.

  Expressions: exp ::= val | var | ptr[exp] | (exp) | u op exp | exp b op exp Unary Operators: u op ::= * | & | ! | -| Binary Operators: b op ::

1 )Figure 4 .

 14 Figure 4. Software pipeline.

Figure 5 .

 5 Figure 5. MicroBlaze multi-core configuration.

Figure 6 .

 6 Figure 6. WCRT results for 802.11a in clock cycles.

TABLE 1 .

 1 FOREC CONSTRUCTS AND THEIR SEMANTICS.

TABLE 2 .

 2 AVERAGE WCRT SPEEDUP RESULTS FOR FOREC AND ESTEREL ON FOUR CORES NORMALIZED TO SINGLE-THREADED C. Because a WCRT analysis technique for Yuan et al.'s approach does not exist, we compare instead the average WCRT speedup achieved by ForeC and Esterel for the following programs: Life simulates Conway's Game of Life for a fixed number of iterations and a given grid of cells. Lzss uses the Lempel-Ziv-Storer-Szymanski algorithm to compress a fixed amount of text. Mandelbrot computes the Mandelbrot set for a square region of the complex number plane. MatrixMultiply computes the matrix multiplication of two equally sized square matrices. Singlethreaded C, ForeC, and Esterel versions of each benchmark program were created and handcrafted for best performance. The same input vector was given to each version to ensure that the same computations were performed. The MicroBlaze simulator returns the execution time when a program terminates.Table2shows the speedups achieved by ForeC and Esterel when the benchmark programs were executed on four cores. Speedup is calculated as:

	Version Life Lzss Mandelbrot MatrixMultiply
	Esterel	2.28	2.42	1.20	3.87
	ForeC	3.25	3.30	3.68	3.76
	MicroBlaze multi-core platform similar to ours. Yuan's ap-
	proach requires a special hardware FIFO queue to help allo-
	cate threads to cores for resolving signal statuses. For bench-
	marking, the MicroBlaze multi-core simulator described in
	Section 2 was extended with a hardware queue to support the
	dynamic scheduling.

TABLE 3 .

 3 AVERAGE SPEEDUP RESULTS FOR FOREC AND OPENMP ON FOUR CORES NORMALIZED TO SINGLE-THREADED C. Because execution is inherently speculative on desktop multi-cores, we present benchmarking results for the average execution time speedup for the following programs: FmRadio [33] transforms a fixed stream of radio signals into audio. The history of the radio signals is used to guide the transformation of the remaining signals. Life and Lzss are desktop versions of those used in Section 6.2.

	Version	FmRadio Life Lzss
	OpenMP	2.02	2.82	3.46
	ForeC	2.63	2.98	3.90
	static schedule.

Acknowledgments

This work was supported in part by the RIPPES INRIA International Lab, and the PRETSY2 project under DFG Funding No. ME 1427/6-2. The authors would like to thank Simon Yuan for setting up the Esterel benchmarks and Avinash Malik for setting up the OpenMP benchmarks.


Functional Electrical Stimulation cycling has numerous benefits for subjects with Spinal Cord Injury. It can improve cardiovascular function, increase muscular mass, and reduce bone mass loss. However, some limitations, e.g. lack of optimal control strategies that would delay fatigue, may still prevent this technology from achieving its full potential. This work tests a control strategy on a complete spinal cord injury subject with a stationary tadpole trike. Two experiments were performed: reference tracking and disturbance rejection. The results show that reference tracking is possible above the cadence of 25 rpm with a mean absolute error lower than 2.5 rpm. The disturbance test showed that it may cause the cadence to drop but still maintain movement if it doesn't get below 25 rpm. When the disturbance is removed, the system is capable of returning the cadence to the initial value.

I. INTRODUCTION

Several studies have presented evidence of benefits that cycling assisted by Functional Electrical Stimulation (FES) may provide to subjects with Spinal Cord Injury (SCI) [START_REF] Davis | Cardiorespiratory, metabolic, and biomechanical responses during functional electrical stimulation leg exercise: Health and fitness benefits[END_REF][START_REF] Deley | Functional electrical stimulation: Cardiorespiratory adaptations and applications for training in paraplegia[END_REF][START_REF] Mazzoleni | Fes-cycling training in spinal cord injured patients[END_REF]. Among the observed improvements, of particular relevance are increased muscular mass, enhanced cardiovascular function, and reduced bone mass loss.

Nevertheless, some limitations within the current technology may still prevent further benefits to the user. For instance, studies have shown that power output obtained using electrical stimulation is reduced when compared to the levels reached using volitional recruitment [START_REF] Kjaer | Cardiovascular and ventilatory responses to electrically induced cycling with complete epidural anaesthesia in humans[END_REF]. Also, the accelerated fatigue induced by FES may prevent achieving higher cardiovascular function improvement.

Those limitations are often associated to features related to motor unit recruitment using surface electrical stimulation. In this scenario, we believe improvements in overall performance may be achieved by applying innovative techniques, such as electrode arrays and asynchronous stimulation [START_REF] Downey | Asynchronous Stimulation With An Electrode Array Reduces NMES-Induced Muscle Fatigue During FES Cycling[END_REF], and complementary control strategies that will enable generation of smooth cycling power patterns.

In our work, the general goal is to investigate new stimulation and control strategies that may improve the overall performance, both in terms of delivered power and fatigue reduction. In a previous work [START_REF] Bó | Experiments on Lower Limbs FES Control for Cycling[END_REF], we have presented results on cycling cadence regulation on healthy subjects. Here, based on similar setup and controller, we present a case study involving one paraplegic subject, as well as results for trajectory tracking and disturbance rejection.

The paper is organized as follows. The next section describes the method, including both hardware and software development, as well as the participating subject and protocol. On the following section the results are presented, as well as the corresponding discussion. Finally, the last section presents the concluding remarks and future works.

II. METHOD

This experimental case study is based on a recumbent tadpole trike adapted for use by paraplegic subjects. The experimental setup, control algorithm, participating subject, and protocol are described below.

A. Experimental setup

The setup was based on an adapted tadpole trike (HP3, Brazil), depicted in Figure 1. The tadpole trike, which features two wheels at the front and one at the back, was chosen for its improved stability when compared to delta tricycles. Among the modifications required for use by paraplegic subjects, supporting surfaces for the whole foot have been attached to each pedal. Also, a vertical rod was rigidly fixed to this structure and the leg in order to secure the limb and prevent residual movements outside the sagittal plane. This structure also kept the ankle joint at 90º at all times.

In addition to the trike itself, a passive cycling trainer was employed to enable indoor and stationary trials. A mechanical assembly was attached to enable instantaneous application of load disturbances to the trainer. As illustrated in Figure 2, increasingly strong disturbances may be applied by using heavier loads.

The electrical stimulation was applied to the quadriceps muscle groups in order to achieve lower limb extension. There was no way to actively induce flexion. However, due to the fixed circular shape of the pedals' trajectory, the extension of one leg led to the flexion of the order, thanks to the bilateral stimulation synchronous timing that was applied.

As for the stimulation unit, a Rehastim (Hasomed, Germany) stimulator was employed. It's an 8-channel current-controlled stimulator that outputs biphasic square pulses. The stimulation parameters (frequency, amplitude, and pulse width) can be updated online through a USB connection. Control algorithms and additional processing are implemented in Python and executed in a personal computer at 25 Hz. The controller receives crank position and angular speed readings from wireless inertial sensors (3space, Yei Technology, United States). The sensing unit is composed of 3-axis accelerometers, gyrometers and magnetometers, and provides measurements of crank position and angular speed based on fusion of data acquired from those individual sensors.

B. Control strategy

Closed-loop control of stimulation pulses is performed using two control loops. As summarized by the diagram depicted in Figure 3, stimulation phases are computed based on crank position and cadence.

Stimulation profile for each pedaling revolution is determined within the inner loop. Computation is defined based on static biomechanical properties of recumbent cycling position with respect to the crank set. Furthermore, stimulation patterns are then adjusted based on cycling cadence, similar to what was proposed by [START_REF] Hunt | Control Systems for Function Restoration, Exercise, Fitness and Health in Spinal Cord Injury[END_REF], to take into account both the artificial and natural delays involved. In order to accomplish that, the system shifts the angular positions in which the stimuli are applied. The faster the cadence, the earlier the stimuli must take place and stop. Furthermore, stimulation intensity (modulated using pulse width in this work) is controlled in order to provide automatic capability to adjust FES level for the required cycling cadence. The goal while providing this functionality is to improve system robustness with respect to different nominal stimulation amplitudes selected within the initialization procedure, which remain constant for the entire duration of the experiment. Also, such control action will react for changes in muscle response, e.g. FES induced fatigue. On this case study, a PI controller is used based on the following parameters: K P = 10 -2 , and K I = 10 -5 . Further details on the overall controller are provided in [START_REF] Bó | Experiments on Lower Limbs FES Control for Cycling[END_REF].

C. Subjects and protocol

After clarification and signing the ethics committee informed consent (CAAE 50337215.1.0000.0030, approval number 1.413.934, February, 18 th 2016), one participant took part in this case study. The volunteer (age: 37 years; height: 1.70 m; body mass: 67.40 Kg) has a complete sensory-motor thoracic traumatic spinal cord injury (T9; AIS A -American Spinal Injury Association Impairment Scale) for 3 years by the time of this work. He is an active athlete, competing on sailing and rowing. Before the tests described here, the subject underwent five months of "pre-training", when he got used to electrical stimulation and increased muscle mass and torque. During that period, he exercised daily with FES for up to one hour and thirty minutes. After that, he did a series of exams to make sure he was able to cycle with FES. These exams analyzed muscle torque, bone density and cardiovascular capacity.

Two protocols were employed. First, there were three trials where the system had to follow a moving reference. It started as a step from 0 instantly to 25 rpm. It maintained that cadence for 13s, and then rose in a ramp up to 42 rpm. After 13s, it lowered to 25 rpm, maintained that cadence for 13s, and then lowered again to rest, always in smooth ramps. These five stages are illustrated on Figure 4. The stimulation current was 40 mA at 50 Hz, and the pulse width was modulated up to 500 µs. The second protocol had the participant cycling at a constant cadence of 33 rpm. At a specific moment, a disturbance was added to the system simulating a slope. After 20s, the disturbance was removed. The disturbance applied on this test was a load of 5.9 Kg. It was introduced at once, and removed also at once. On all cases, the stimulation was applied in a trapezoidal shape. In other words, when it was time to stimulate, the pulse width rose from 0 µs to the specified value by the controller in a ramp. When it was time to stop de stimulation, it also lowered in a ramp. These ramps were set in a manner that right and left leg stimulations overlaped. It has been noticed that such strategy produced smoother movements and, on healthy subjects, more confortable sensations.

III. RESULTS

The experimental results obtained during this case study are depicted in Figures 4567.

During the reference tracking without disturbance experiment, the system followed the reference with an absolute mean error within 2.5 rpm for most of its execution. During the first stage, where the system is supposed to follow the cadence of 25 rpm, and on the last one, stopping, the error was larger. On the stopping stage of the second trial there was a much higher error when compared to the other stages and trials. These results are illustrated on Figure 6. Figure 4 represents one of the reference tracking tests results.

On the disturbance experiment, the pre disturbance stage error result was similar to the cadence of 25 rpm from the previous experiment when the absolute mean error is observed, and the post disturbance stage had a slightly better performance. During the disturbance, the error was larger than on the other stages. These results are illustrated on

IV. DISCUSSION

Although this study involved only one SCI subject, the obtained results enable discussing some of the method's advantages and limitations.

During the reference tracking experiment, the target cadence ranged from 25 rpm to 42 rpm. The absolute mean error between 0.8 and 2.5 rpm observed on most stages and trials on Figure 6 represents a low error. Since the system stimulates only the quadriceps, the cycling pattern is achieved through pushing the pedals in a controlled timing. However, after an extension of one leg (and flexion of the other), there are no stimuli for the remaining of the movement until it's time for the next leg to extend. For that reason, the crank keeps on rotating only due to the acquired inertia during the previous extension, so the measured cadence on that moment is lower than when the stimulation is taking place. This is visible on Figure 4 by the oscillating aspect of the graph. Every peak is a leg being stimulated, and every valley is the moment when there's no stimulation. Most of the error is due to this effect, which happens also with healthy subjects practicing regular cycling, and should be minimized in order to improve performance.

The reference cadence of 25 rpm was chosen because it is a cadence with which the cycling movement was stable. Below that the participant could get stuck between extensions due to the low inertia. That's why the beginnings of the trials are not ramps, but steps. With an instant step to 25 rpm, the controller initial proportional channel is high due to the high error, making the controller start at a high intensity stimulation, achieving the required inertia quickly. As is expected from a PI controller, the cadence takes some time to settle on the reference, making the error values for the first stage higher than the others. The last stage, stopping, however, has reference cadences below 25 rpm, which often causes the highest errors.

At the disturbance test, the system wasn't capable of successfully rejecting it. On the other hand, it was able to maintain the cycling pattern, although below the reference cadence. However, if the cadence had dropped below 25 rpm, the systems would probably stop, as previously explained. During the time in which the disturbance was applied, the stimulation was saturated, meaning it was requiring maximum effort from the muscles with that current. After the disturbance was removed, the cadence took some time to get back to 33 rpm. We suspect it happened because the muscles got slightly fatigued due to the saturation, but quickly recovered and could reach the reference cadence again.

During normal cycling practice, when facing a slope or some kind of resistance, the pilot could lower the gears and would probably be able to keep cycling.

V. CONCLUSION

This study case showed that the presented set-up and the developed control strategy is capable of tracking a moving cadence reference for FES cycling, as long as it doesn't drop below 25 rpm. However, the cadence oscillates considerably, and this leads us to pursue ways to make it smoother. [START_REF] Hunt | Control Systems for Function Restoration, Exercise, Fitness and Health in Spinal Cord Injury[END_REF] and other works propose the electrical stimulation of hamstrings and gluteus, along with quadriceps, and a more complex synchronization pattern in order to achieve torque on all crank positions, reducing this oscillating effect.

The disturbance test showed that a disturbance load can affect the cadence in a way that the presented strategy is unable to recover while the load is present. The pilot can keep on cycling and even recover the target cadence if he/she notes it and lower the gears. Therefore, one solution would be to ensure it making this information available, e.g. on a screen. Another solution would be to automate the gears' switching according to the load, crank speed and muscle effort.

The main goal of this work was to evaluate whether our control system was able to reject load perturbations and follow accelerating and decelerating reference cadences. After the tests, some opportunities for improvement were identified. At the same time, our work group is preparing 14 other subjects for further experiments, which will help us analyze our control strategies in comparison to others in the literature. Also, other important variables will be tested, e.g. the influence of SCI chronicity, SCI level, and mechanical aspects.

Besides the stimulation of more muscle groups, future work include the trike's further instrumentation for outdoors cycling. In order to do that, it will have all devices embedded, including the computational unit, electrical stimulator and power sources. Also, brake sensors will be used to stop stimulation during braking to avoid unnecessary effort. Finally, force sensors on both pedals will give precise feedback of each leg torque contribution, allowing the system to independently modulate the stimulation for each one. This should be useful in case one leg is stronger than the other, or fatigues faster.

*

  Research partially supported by CAPES, CNPq, INRIA and FAPDF. L. O. da Fonseca, Antônio P. L. Bó, J. A. Guimarães, Miguel E. G. Paredes, and Emerson Fachin-Martins are with the University of Brasília, Brasília, Brazil (e-mail: lucasfonseca@lara.unb.br). Ulisses de Araújo is with CETEFE, Brasília, Brazil. C. Azevedo-Coste is with CAMIN, LIRMM/INRIA, Montpellier, France.

Figure 1 .

 1 Figure 1. The tadpole Trike used in this work.

Figure 2 .

 2 Figure 2. Trike schematic illustrating the mechanism design to apply disturbance load.

Figure 3 .

 3 Figure 3. Block diagram illustrating controller composed by two control loops that computes stimulation timing and intensity.

Figure 7 .

 7 Figure 7. Figure 5 represents one of the disturbance rejection tests results.

Figure 6 .Figure 7 .

 67 Figure 6. Reference tracking results

Figure 4 . 1 Figure 5 .

 415 Figure 4. Reference tracking results, trial 1

ACKNOWLEDGMENT

We would like to thank the participating subject, who continuously motivates us to continue our development effort. We would also like to thank the NTAAI -Núcleo de Tecnologia Assistiva, Acessibilidade e Inovação from FCE-UnB.