From Lyra

Contents 1 Overview 2 Rationale 2.1 Rendezvous 2.2 EFSM 3 The Lyra Model 3.1 Example: Dining Philosophers 3.2 Example: Elastic Pipeline Stage 3.3 Example: Ticket Masters 4 Related Work 4.1 Concurrent Programming Languages 4.2 FSM Models 4.3 Bluespec 5 Challenges 5.1 Scalability of multiparty scheduling 5.2 Implementation 5.3 Acceptance by designers 6 Acknowledgments 7 References

Overview

Lyra is a concurrent programming model based on the finite state machine theory and rendezvous-style communication. It is also the name of the hardware modeling language that is based on the Lyra model. Lyra's main purpose is to model digital hardware at high abstraction levels. It aims to bridge the semantic gap between the transaction level (TL) and the register transfer level (RTL). Currently at the ECE Department of Boston University, we are actively working on the theoretical aspects of the model and implementing the related tools. Our goal is to create a framework that models, synthesizes and verifies digital hardware at TL.

Lyra is named after its namesake constellation. In ancient Chinese legend, Lyra is a cloud-weaving maid (Vega) with her weaving shuttle. She is separated by the Milky Way from her herdboy husband (Altair) and two children (Alshain and Tarazed). They are allowed to have a rendezvous on July 7th of each lunisolar year.

Rationale

Many recent ESL tools adopt high-level programming languages such as C++ for quick development of functional models at TL or higher. Although some tools provide limited synthesis capability, TL models are generally considered not synthesizable. Circuits are still predominantly implemented in hardware description languages (HDLs) at RTL. The duplicate modeling and implementation effort leads to not only wasted productivity, but also the extra burden of verification between the model and the implementation. We believe the gap between modeling and implementation is largely due to the fact that the current ESL tools focus primarily on design languages, but sidestep the fundamental problem of formal modeling. A successful ESL tool needs to have a formal theoretical foundation that is sufficiently versatile for different levels of abstraction between TL and RTL. Unfortunately, none of the well-studied models of computation (MoCs) meets the requirement. For instance, the well-known discrete-event (DE)^[1] model is sufficiently general to model digital hardware at the gate level or above, but is not capable of representing the communication primitives at the transaction level. High level models such as the Kahn Process Network (KPN)^[2] or the Communication Sequential Process (CSP) ^[3] are convenient at the transaction level but lack the expressiveness for fine-grained resource contention and arbitration at the microarchitecture level or RTL.

The Lyra model aims to close the gap. It models transactions using rendezvous, which is a formal and flexible means for inter-process communication. It uses the familiar extended finite state machine (EFSMs) model to represent processes, whose explicit representation of control flow is convenient for composing rendezvous. The combined expressiveness of rendezvous and EFSM allows Lyra to model hardware at any level from RTL to TL.

Rendezvous

Rendezvous is a synchronous handshaking mechanism among processes. In its simplest form, two processes waits for each other at a rendezvous point when they expect to handshake. When both parties are all present, the rendezvous occurs, allowing both processes to continue to progress. Rendezvous may also serve as a medium of communication. Data values can be exchanged between the processes as the rendezvous occurs.

Rendezvous appeared in concurrent programming languages such as Ada^[4], Occam^[5], and Lotos^[6], as well as in process calculi such as CSP^[3] and CCS^[7]. Recently in EDA area languages such as Handel-C^[8], Haste^[9] and SHIM^[10] were proposed to model hardware and systems. Compared to function-call-style transactions, rendezvous offers the following advantages:

• Rendezvous connect processes directly, vs.
  functions connect processes indirectly via shared variables or message channels;
• Rendezvous are symmetric and only occur when involved parties agree to participate, vs.
  functions give callers full control of invocation;
• Rendezvous support multipartiness, vs.
  functions involve only two parties in every invocation.
• Rendezvous allows parallel composition, vs.
  functions are sequential and do not support composition.

Because of the above, rendezvous are more expressive than functions for modeling inter-process communication in concurrent systems such as digital hardware. Note that the synchronicity of rendezvous means that all parties of a rendezvous will wait for its occurrence before continuing, but is not related to the timing of implementation. It has been used to design both synchronous and asynchronous hardware in the past.

EFSM

EFSMs are FSMs with additional internal data storage. An EFSM is a single sequential process, with its control flow and data actions exposed by the state diagram. The explicit state diagram structure is suitable for IPC based on multiparty rendezvous, which requires individual processes to expose their intention to the central scheduler. Though in theory any style of sequential process satisfies our purposes so long as it fully exposes its IPC, we prefer EFSM since it has long been used for designing digital hardware and is thus familiar to hardware designers.

The Lyra Model

The Lyra model uses rendezvous to connect communicating sequential processes. The processes are represented using state diagrams so that their control flows are explicit. The edges of the state diagrams are labeled with required rendezvous, Boolean expressions as guarding conditions, and statements as the actions to take when transitions occur. For a state transition to take place along an edge, all rendezvous on the edge must occur and the Boolean expression on the edge must be true. When a transition takes place, all rendezvous and statements on an edge occurs atomically.

The model supports two types of rendezvous:

1. Bi-party rendezvous called rendv. A rendv involves one or more producers, and one or more consumers. In each occurrence, exactly one producer and one consumer participate.
2. Multiparty rendezvous called barrier. Each occurrence of a barrier requires all parties to participate.

The choice of these two types of rendezvous is based on the need for system modeling with an emphasis on hardware. Rendv models resource transactions, which may involve choice from multiple producers or competition among multiple consumers. Barrier models group synchronization among several processes. It can be used to represent a clock or a global reset signal. Despite their different appearance, the two rendezvous types nicely fit into the same mathematical framework^[11].

Additionally, Lyra supports the following features:

1. Both disjunctive and conjunctive composition of rendezvous are supported.
2. Rendezvous may carry bidirectinoal data flow.
3. Dataflow spans across conjunctively composed rendezvous. In other words, the input data of one rendezvous may be forwarded to another rendezvous instantaneously.
4. Processes in general update in an asynchronous fashion. Different processes may update at different paces. They only synchronize when rendezvous occur among them.

Below are a few examples illustrating the usage of the model showing the capability of the model. All rendezvous in the examples are rendv's since it is the most commonly used type. The dining philosophers example shows the conjunctive composition of rendezvous. The elastic pipeline example shows both conjunctive and disjunctive composition of rendezvous, as well as data flow through the pipeline. The last example shows competition of rendezvous parties and data conditions.

Example: Dining Philosophers

The dining philosophers problem is a classic multi-process synchronization problem illustrating deadlock and starvation. "The dining philosophers problem is summarized as five philosophers sitting at a table doing one of two things: eating or thinking. While eating, they are not thinking, and while thinking, they are not eating. The five philosophers sit at a circular table with a large bowl of spaghetti in the center. A fork is placed in between each philosopher, and as such, each philosopher has one fork to his or her left and one fork to his or her right. As spaghetti is difficult to serve and eat with a single fork, it is assumed that a philosopher must eat with two forks. The philosopher can only use the fork on his or her immediate left or right."^[12]

The problem can be modeled as 5 philosopher processes p_i and five fork processes f_i, where i ∈{0,1,2,3,4}. They synchronize via rendezvous get_i and ret_i (get₅ is the same as get₀, ret₅ is the same as ret₀). Get_i means to acquire a fork, and ret_i means to return a fork. Every rendezvous has two roles, a "+" role for the philosopher, and a "-" role for the fork.

Under the Lyra approach, a philosopher can be modeled as the shown process p_i. A philosopher moves from "think" to "eat" only when he/she acquires both forks simultaneously. He/she returns both forks simultaneously when done.

A fork can be modeled as the shown simple process f_i. It can be either in use of free.

The simultaneous occurence of both gets of a philosopher prevents deadlock from happening. However, starvation may still occur if the scheduler is deterministic.

Example: Elastic Pipeline Stage

An elastic pipeline allows "bubbles" to exist. If one stage is blocked, its downstream stages can still advance, creating a bubble in its immediate next stage. And its upstream stages may also advance by "squeezing" the bubbles in upstream stages. For example, if a 7-stage elastic pipeline has stage 1, 2, 5, 6 occupied, and stage 5 is blocked, then the data in stages 1, 2 and 6 can still advance into stages 2, 3 and 7, respectively. After that, stage 6 will have a "bubble". Stage 1 may or may not get a "bubble" depending on whether new data comes into the pipeline. The example is illustrated below.

Original
Updated

Each stage of the elastic pipeline can be modeled by a simple process shown on the right. State empty means the stage is unoccupied, and full means otherwise. As for the process representing stage i, it is connected to the preceding stage by rendezvous prop_i, and to its following stage by rendezvous prop_i+1. It has an internal state variable v for storing the data. In the aforementioned example, rendezvous prop₂, prop₃ and prop₇ occur simultaneously, causing the following changes.

1. Process 1 moves from Full to Empty or Full, depending on whether new data is given by prop₁;
2. Process 2 moves from Full to Full along the right-most edge;
3. Process 3 moves from Empty to Full;
4. Process 6 moves from Full to Empty;
5. Process 7 moves from Empty to Full.

A more powerful elastic pipeline stage can include an additional cyclic edge around the Empty state, as shown in the figure below. The statement on the edge forwards the data received from prop_i^- directly to prop_i+1⁺, causing a data element to bypass an empty stage in such a pipeline. In the aforementioned example, data in stage 2 can directly advance to stage 4 in one hop, as shown below.

Original
Updated

The changes involved are:

1. Process 1 moves from Full to Empty or Full, depending on whether new data is given by prop₁;
2. Process 2 moves from Full to Full along the right-most edge;
3. Process 3 moves from Empty to Empty along the left-most edge;
4. Process 4 moves from Empty to Full;
5. Process 6 moves from Full to Empty;
6. Process 7 moves from Empty to Full.

A less powerful elastic pipeline stage will have only the two middle edges. In the aforementioned example, data in stage 2 can advance to stage 3 since stage 3 is currently empty. But data in stage 1 will have to wait for stage 2 to become empty before moving into stage 2. This type of pipeline can only be half-full when working in full speed. In other words, its highest throughput is 1 data every two cycles.

Example: Ticket Masters

This example illustrates the bi-directional data flow through rendezvous. In this example, several customers are purchasing tickets from several ticket masters. Each customer has an age value, and a variable money which decrements in a purchase. Each ticket master checks if the customer's age is greater than 18, and if so, gives a ticket to the customer from his pile of tickets t[], and increments his/her money count. A ticket master can sell at most 20 tickets.

The problem can be modeled by several customer processes and several ticket master processes. Their transactions are through a set of rendezvous ticket_i, one for each ticket master. A customer process is shown on the right. The customer has the choice of buying from any ticket master. The right pointing edges in the figure correspond to the choices. Each edge is guarded by a check of money, and the occurrence of the ticket_i rendezvous. If the corresponding ticket master does not want to trade with the customer, either because the customer is underage, or the ticket master is busy with another transaction at the moment, or because the ticket master runs out of ticket already, the edge is not enabled. If an edge is enabled, then a transition may occur along the edge. The customer will receive the ticket t, and decrement the money. The customer keeps buying until the money runs out.

A ticket master process is shown below. The ticket master will probe and check the age value from the rendezvous ticket_i, checks the ticket count, and sends the ticket to the customer, all as one atomic event.

In this example, The connectivity between customers and ticket masters resembles a crossbar. A rendezvous may occur between any customer/ticket master pair, if the following conditions hold:

1. The customer has money;
2. The customer is above 18;
3. The ticket master has not reached the limit of 20.

The check of the conditions, the occurrence of the rendezvous, and the update of variables are one atomic event. The rendezvous carries data in both directions: the age information from the customer to the ticket master, and the ticket from the ticket master back to the customer. The age information is used to guard the transaction.

A simpler model can combine all the ticket_i into one rendezvous. All the right pointing edges in the customer process can be merged into one. The simplified model allows only one transaction at any moment.

Related Work

This section compares Lyra to existing work in related fields.

Concurrent Programming Languages

Many concurrent programming languages uses rendezvous-style communication. These include Ada^[4], Occam^[5], Lotos^[6], Handel-C^[8], Haste^[9], and SHIM^[10]. Among these, Occam, Handel-C and Haste are all based on CSP^[3], though their support for some aspects of rendezvous differs. Lotos is based on extended CCS^[7] and CSP. It is intended as a specification language, but not a real programming language.

The languages differs in their support of the following features:

1. Multipartiness - the number of parties involved in each occurrence of a rendezvous
2. Variability - whether the participating parties of a rendezvous must be a fixed set of processes or a variable subset
3. Disjuncton - whether rendezvous can be used in disjunction so that one of several choices should occur
4. Conjunction - whether rendezvous can be used in conjunction so that several rendezvous must jointly occur
5. Flow of data - the direction of data flow along with the occurrence of a rendezvous

The table below compares the features of the above languages.

Comparison of Features

Language	Multipartiness	Variability	Disjunction	Conjunction	Dataflow
Ada	No	"caller" only	Yes	No	2-way
Occam	No	No	Yes	No	1-way
Handel-C	No	No*	Yes	No	1-way
Haste	"Broadcast"	"Narrowcast"	Yes	Yes	1-way
Lotos	Yes	No	Yes	No	multi-way
SHIM	Yes	No	No	No	1-way
Lyra	"Barrier"	"Rendv"	Yes	Yes	2-way

"*" Handel-C's variability should be resolved by progammer, as the LRM states that "No two statements may simultaneously write to or simultaneously read from a single channel". So its "variability" does not cause nondeterminimsm, and thus not considered here.

Feature-wise, Lyra is most similar to Haste. Both support the same types of rendezvous, the same styles of variability, and similar styles of composition. The major difference between the two is the their treatment of probing. In Haste, a process can probe a narrowcast channel to see if a counterparty is ready for a rendezvous. Probing is required to implement disjunctive composition (the select statement), or conditional guards based on input values. Since the probe and the actual rendezvous are two separate events, it may happen that the status of the channel changes between the two: the probe succeeds but the actual handshake fails. Thus programmers need to ensure that for each probed channel, the counterparty must be committed to the rendezvous, and there is no interference from competitors for the channel. Therefore, it is impossible to model the ticket master example using Haste. Lyra does not have such limitation.

Another difference between Lyra and Haste is the data flow. Lyra allows bidirectional flow of data in rendezvous, while Haste supports unidirectional data flow. Lyra allows data to go across conjunctively composed rendezvous instantaneously, i.e. the input received from one rendezvous can be relayed to the output of another instantaneously, as in the left-most edge of the aforementioned elastic pipeline with bypassing capability. In Haste, this is not supported.

FSM Models

Several high-level FSM models have been introduced for modeling above RTL. They typically use events (or messages) buffered by event queues (or message channels) for communication. These variants include the communication FSM^[13] primarily used for communication protocol modeling, behavioral FSM ^[14] for behavioral synthesis, codesign FSM^[15] for hardware/software codesign, Harel's Statecharts^[16] for software specification, and the Operation State Machine (OSM)^[17] for modeling operation flow in a processor.

In all but OSM, the communication primitives are unidirectional among FSMs. To model a bidirectional handshake between two processes, at least two separate events are involved. In contrast, OSM uses function-call transactions and allows a bidirectional handshake in one atomic transaction. However, OSM is not a complete model because it only represents the flow of operations in a processor. Another layer of hardware resources must be used to complement the model. Lyra generalizes OSM by replacing function calls with rendezvous. Lyra is complete and can model any logic hardware.

Bluespec

Bluespec is a high-level design language based on the theory of term-rewriting systems (TRS)^[18]. A module in Bluespec makes progress according to a set of atomic rules. A rule reads and updates the states of the owner module, and may also read and update the states of other modules by invoking their exported methods. The Bluespec compiler analyzes the conflict between all rules and ensures that the system progresses in a race-free manner. The rule-based modeling style of Bluespec is very different from the process-oriented style of FSM models. It does not explicitly expose the control flow of processes. Instead, Bluespec synthesizes control paths automatically, allowing designers to focus on specifying computation.

The main difference between Bluespec and Lyra is that Bluespec does not give designers full flexibility in controlling the firing of the rules (e.g. to explicitly request two rules to fire together). It is not possible to compose the rules freely in a conjunctive manner. Thus it is not as straightforward to express the two aforementioned elastic pipeline diagrams in Bluespec. In addition, Bluespec does not explicitly express the control flow structure of a process and thus is less convenient in modeling multi-step processes involving branching and merging.

Challenges

Without challenges, this project would not have been interesting.

Scalability of multiparty scheduling

In general, scheduling in the presence of only fixed multipartiness and disjunction is trivial. Individual processes can progress independently using only local knowledge. On the other hand, variability and conjunctive composition generally require the use of arbitration and coordination. Variability enables competition to be specified, implying the need of arbitration. Conjunction composition teams up multiple processes, implying the need of coordination. However, the past languages avoid multiparty scheduling by placing restrictions on their use of rendezvous. For example, Handel-C requires that no two processes should write to the same rendezvous channel simultaneously, leaving the burden of arbitration to programmers. Haste supports limited arbitration of channels, but does not further coordinate the processes when variability and composition coexist, leaving many deadlock hazards for programmers to deal with.

Lyra takes on the task of global scheduling. In the worst case, assuming full connectivity of all processes and all rendezvous, the complexity of of the scheduler is exponential. Fortunately, real-world systems have reasonable connectivity, and can be divided into subsystems. We have identified a few scheduling algorithms that are highly scalable in practice. The results are being summarized and to be published.

Implementation

The advantage of function-call based concurrency is that it does not affect the programming language. A concurrency library is sufficient for extending a sequential language. Rendezvous-based concurency, on the other hand, always require a new language. So a huge amount of effort has been spent on defining a language, implementing the compiler and the reference simulator. We tried hard to make the language familiar to C and Verilog programmers. The work is near completion, though some aspects of the language still need to be cleaned up.

Acceptance by designers

Most programmers are not familiar with rendezvous since few mainstream languages use rendezvous nowadays. As a matter of fact, few mainstream languages support inter-process communication (IPC) directly at the language level. The situation may change in the near future as more resources are being spent on parallel programming in the multi-core and many-core era. We expect in the near future more designers will be used to programming with rendezvous.

Acknowledgments

We cordially thank Freescale Semiconductor for generously supporting this project via the SRC grant 1622.

References

1. ↑ Banks, Jerry, Carson, John, Nelson, Barry, and Nicol, David. Discrete-event system simulation. Prentice Hall, 2004.
2. ↑ Kahn, G. The Semantics of a Simple Language for Parallel Programming. In Proceedings of International Federation for Information Processing Congress, 1964, 471-475.
3. ↑ ^{3.0 3.1 3.2} Hoare, C.A.R. Communicating Sequential Processes. Prentice Hall, 1985.
4. ↑ ^{4.0 4.1} ISO/IEC(8652:1995). Ada Reference Manual - Language and Standard Libraries. 1995.
5. ↑ ^{5.0 5.1} Barrett, Geoff. Occam3 reference manual. INMOS Ltd., 1992.
6. ↑ ^{6.0 6.1} Bolongnesi, Tommaso and Brinksma, Ed. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, Vol. 14, No. 1, January 1987, 25-59.
7. ↑ ^{7.0 7.1} Milner, R. Communication and Concurrency. Prentice Hall, 1989.
8. ↑ ^{8.0 8.1} Celoxica Ltd. Handel-C Language Reference Manual. 2005.
9. ↑ ^{9.0 9.1} Handshake Solutions, Haste Programming Language Manual, 2008.
10. ↑ ^{10.0 10.1} Edwards, Stephen A and Tardieu, Olivier. SHIM: A Deterministic Model for Heterogeneous Embedded Systems. IEEE Transactions on Very Large Scale Integration Systems, Vol. 14, No. 8, August 2006, 854-867.
11. ↑ Qin, Wei. Refined Theory of Rendezvous Finite State Machine. Technical Report , ECE Department, Boston University, 2008. http://people.bu.edu/wqin/pdf/techrep-rfsm2.pdf.
12. ↑ http://en.wikipedia.org/wiki/Dining_philosophers_problem
13. ↑ Peng, W. Deadlock detection in communicating finite state machines by even reachability analysis. Mobile Networks and Applications, Vol. 2, No. 3, December 1997, 251-257.
14. ↑ Takach, Andres, Wolf, Wayne, and Leeser, Miriam. An Automaton Model for Scheduling Constraints in Synchronous Machines. IEEE Transactions on Computers, Vol. 44, No. 1, January 1995, 1-12.
15. ↑ Chiodo, M., Giusto, P., Hsieh, H., Jurecska, A., Lavango, L., and Sangiovanni-Vincentelli, A. A formal specification model for hardware/software codesign. In Proceedings of the International Workshop on Hardware-Software Codesign, 1993.
16. ↑ Harel, David. Statecharts: A visual formalism for complex systems. Science of Computer Programming, Vol. 8, No. 3, June 1987, 231-274.
17. ↑ Qin, Wei and Malik, Sharad. Flexible and Formal Modeling of Microprocessors with Application to Retar. In Proceedings of Conference on Design Automation and Test in Europe, 2003, 556-561.
18. ↑ Nikhil, Rishiyur. Bluespec: A General-Purpose Approach to High-Level Synthesis Based on Parallel Atomic Transactions. In Philippe Coussy, Adam Morawiec, ed., High-Level Synthesis - From Algorithm to Digital Circuit. Springer, 2008.