=Paper= {{Paper |id=Vol-1689/paper15 |storemode=property |title=Model-based Design and Formal Analysis of Arbitration Protocols on Multiple-Bus Architecture |pdfUrl=https://ceur-ws.org/Vol-1689/paper15.pdf |volume=Vol-1689 |authors=Imene Benhafaiedh,Maroua Ben Slimane |dblpUrl=https://dblp.org/rec/conf/vecos/BenhafaiedhS16 }} ==Model-based Design and Formal Analysis of Arbitration Protocols on Multiple-Bus Architecture== https://ceur-ws.org/Vol-1689/paper15.pdf

Model-based Design and Formal Analysis of
Arbitration Protocols on Multiple-Bus
Architecture

Imene Ben-Hafaiedh1 and Maroua Ben Slimane2
1
Higher Institute of Computer Science (ISI), LIP2 Lab
2
Tunisia Polytechnic School, LIP2 Lab

Abstract. Multiple-Bus architectures for multiprocessors systems are
preferred by manufacturers for implementation as they are providing
higher bandwidth and more reliability than single bus architectures. The
key notion in such a multiple-bus system is the bus arbitration strategy
which resolves request conicts and allocates buses to requesting de-
vices. Indeed, fast and fair bus arbitration gives higher throughput and
less queuing time. In this paper we propose a high-level formal model of
multiple-bus multiprocessor architecture seen as a component-based sys-
tem. The proposed model oers a way to easily implement, analyze and
compare dierent arbitration protocols using a rich notion of connectors
between components. This model allows to study relevant properties
such as fairness and deadlock freedom at a high level of abstraction.
Moreover, the proposed model of the studied protocols is modeled in
a distributed manner which makes the generation of their implementa-
tion more interesting and the study of their performance eciency more
relevant.

Key words: Formal Model, Multiple-bus architecture, Distributed Model,
Arbitration Protocols

1 Introduction

In multiprocessors systems (MPSoC), heterogeneous components (processors,
memories, logics, DSPs...) are integrated into a single chip. That is why the
performance of these systems depends more on ecient communication among
these devices. In general, this communication ensures access to shared resources.
In the case of multiple bus architectures, such devices share a limited number
of buses. The access to these shared buses is managed by a bus arbiter that re-
solves request conicts and allocates buses to requesting devices. The eciency
of these systems depends considerably on the protocol used by the arbiter for
bus allocation and how this protocol could be balanced and time ecient. Thus,
the choice of the arbitration protocol plays an essential role in deciding the per-
formance of bus based systems [1,2,3,4].
Multiple bus systems performance could be guaranteed by adopting eective bus
arbitration protocols (policies) which could ensure several requirements such as
deadlock freedom, fairness, simplicity and time eciency [5,1]. Analyzing prop-
erties of these dierent protocols at a high-level system description is useful for
comparing their performance without having to go into very low-level implemen-
tation details. We claim that arbitration protocols could be naturally specied
by expressive high-level features such as Connectors and Glues specifying rich
interaction models between the dierent devices. Such features are provided by
several component-based frameworks like those described in [6,7,8]. In [7], such
rich interaction models allow the description of the dierent protocols based on
high-level expressive notions like multi-party interactions and global priorities.
The use of these notions leads to much more concise specications which are
more adequate to provide a comprehension of the global behavior of the dier-
ent protocols and for the verication of their global properties. In [9], a similar
approach has been proposed, however this approach was limited to a single bus
architecture. In the present work, we propose a high-level analysis approach for
systems with multiple-bus multiprocessors architecture which makes the arbi-
tration protocols completely dierent with more interesting issues to take into
account. Moreover in such multiple bus architectures, distributed conguration
and implementation become more interesting.
Indeed, in multiple bus protocols there are two types of conicts to manage.
First, a conict between processors to get a bus access. Second, a conict be-
tween buses, which is not taken into account in [9]. In this paper, our rst aim
is to propose a way allowing to decide at a high-level about the appropriate
arbitration protocol to implement. This choice is in general related to a set of
requirements and properties (fairness, time eciency, ...). Thus if such proper-
ties could be studied at a high-level, one can decide about the protocol to use
without having to go into low level implementation details.
To reach this purpose, we propose an abstract formal model of multiple-bus ar-
chitecture using a component based framework named BIP (Behavior-Interaction-
Priority) [7,10]. This framework oers an expressive interaction model based
on a rich notion of glues called connectors [11] [12] and an interesting notion of
priority between interactions [13].
Based on these notions, we propose a model to describe, in an elegant manner
the multiple bus architecture for three well-known arbitration protocols namely
xed, equal and rotating priority protocols.

The second contribution of this paper is the distributed aspect of the pro-
posed model. In fact, our model is designed in a distributed manner, which
means that a set of local arbiters, associated each to a device, control the access
to the dierent buses. Such a model makes a distributed implementation easily
generated. Thus a set of experimental results are then easily obtained to allow
protocols eciency studies.
The rest of this paper is organized as follows: In Section 2, we give an
overview about the component-based (BIP) framework adopted to design the
proposed high-level model. Then, in Section 3, we describe our proposed ab-
stract and formal model for multiple bus architecture and how this model can
be parameterized to dene several well-known arbitration protocols. Section 4
presents some experimental results obtained from our automatically derived im-
plementation. In Section 5, we compare our work to some existing researches.
In Section 6, we sum up and discuss possible perspectives.

2 BIP Framework

In this section, we present a high-level modeling formalism for the description
a multiple bus network architecture. We choose to specify our model using
the BIP (Behavior-Interaction-Priority) component framework [7] [12] as it is a
framework with formal semantics that relies on rich interaction models between
components [11]. These interaction models are based on multi-party interactions
for synchronizing components and in particular priorities for scheduling between
interactions [13]. Moreover, this framework provides dierent tools for property
verication and distributed code generation.
Denition 1 (Atomic component). An atomic component K is a Labeled
Transition System (LTS) dened by a tuple (Q, V, P, δ, q0 ) where Q is a set of
states,V is a nite set of variables, P is a set of communication ports, a transi-
tion relation δ ⊆ Q × P × Q and qo ∈ Q is the initial state.
As usually, q1 −→ q2 denotes (q1 , a, q2 ) ∈ δ
a

In practice, each variable may be associated to a port and modied through
interactions involving this port. We also associate a guard and an update function
to each transition. A guard is a predicate on variables that must be true to
allow the execution of the transition. An update function is a local computation
triggered by the transition that modies the variables. Atomic components in
BIP interact using interactions.
Denition 2 (Interaction). Given a set of n atomic components Ki = (Qi , Vi ,
Pi , δi , qoi ) for i ∈ [1, n], in order to build their composition, we require their sets
of ports to be pairwise disjoint, i.e. for Sany two i 6= j from [1, n], Pi ∩ Pj = ∅.
The composed system is dened on P = ni=1 Pi and the set of its ports is dened
by a set of interactions. An interaction a is dened by a non empty subset of
P representing a joint transition of the set of transitions labeled by these ports.
Note that each interaction denes itself a port of the composition which is useful
for dening systems hierarchically (Denition 3).
Composition of components allows to build a system as a set of compo-
nents that interact by respecting constraints of an interaction model. In BIP
interactions are structured by connectors. A connector is a macro notation for
representing sets of related interactions in a compact manner. To specify the
interactions of a connector, two types of synchronizations are dened:
strong synchronization or rendez-vous, when the only interaction of a con-
nector is the maximal one, i.e., it contains all the ports of the connector.
weak synchronization or broadcast, when interactions are all those containing
any port initiating the broadcast.
To characterize these two types of synchronizations, a connector may associate
to the ports it connects two types:
A trigger port of a connector is a complete port which can initiate an in-
teraction without synchronizing with other ports of the connector. It is
represented graphically by a triangle.
A synchron port of a connector which is an incomplete port, hence needs
synchronization with other ports, and is denoted by a circle.
Let γ be a connector connecting a set of ports {pi }ni=1 , then γ is dened as
follows:
Denition 3 (Connector). A connector γ is dened as a tuple (pγ [x], Pγ , δγ )
where:
pγ [x] is a port called the exported port of γ with x as associated variable,
Pγ = {pi [xi ]}ni=1 is the set of connected ports called the support set of γ .
These ports are typed by the information whether they are trigger or synchron
port. xi is a variables associated to pi .
δγ = (G, U, D) where,
• G is a guard of γ , an arbitrary predicate G({xi }i∈[1,n] ),
• U is an upward update function of γ of the form, x := F u ({xi }i∈[1,n] ),
• D is a downward update function of γ of the form, ∪pi {xi := Fxdi (x)}.
The intuition behind the notion of exported port, as illustrated in Figure 1, is
that a connector allows to relate a set of inner ports (of connected components) to
a new port (the exported port) which allows to provide a notion of encapsulation
by dening the interface of the obtained composite component. The composition
pγa pγb

p1 p2 p1 p2

(a) (b)

Fig. 1. Example of Connectors.

of BIP components with a connector γ denes an LTS (Denition 4).
Denition 4 (Composition of components). The composition of n com-
ponents Ki by a connector γ is denoted by K = γ(K1 , ... , Kn ) and it denes
an LTS (Q, P, δ) such that Q = ni=1 Qi and δ is the least set of transitions
Q
satisfying the following rule:
pi
a = {pi }i∈[1,n] , ∀i ∈ [1, n]. qi1 −→ qi2 ∧ ∀i 6∈ [1, n]. qi1 = qi2
a
(q11 , ... , qn1 ) −→ (q12 , ... , qn2 )
The Denition 3 of connectors represents connectors which are essentially at,
i.e., having types (triggers and synchrons) associated to the individual ports
(support set) only. However, connectors sometimes need to be structured, i.e.,
having types associated to groups of ports. This is necessary to represent some
interactions, which otherwise cannot be represented by a at connector. Struc-
tured connectors are created by the combined mechanism of exporting port from
a connector and instantiating connectors, where a port of the connector is an
exported port of another instantiated connector.
This is called domination [11]. That is, γi dominates γj means that the
exported port of γj belongs to the support set of γi (see Figure 2).

Fig. 2. Dominance between connectors.

The purpose of this work is to provide a formal high level model of multi-
ple bus architecture. Using the dierent features oered by BIP, in particular
connectors, we propose a way to easily model, study and compare dierent ar-
bitration protocols.

3 Distributed model of multiple-bus architecture

Our purpose is rst to provide a formal model for a multiple-bus architecture.
Then, based on this model, dierent arbitration protocols could be easily mod-
eled and analyzed. Using the notions of BIP framework already described in
Section 2, we propose to model a multiple-bus architecture by dening the set
of processors as a set of BIP atomic components. Comparing to the model pre-
sented in [9], we are here interested in multiple-bus and not a single one, thus,
we use also a set of BIP atomic components to model the set of shared buses.
In the case of a centralized setting, a single centralized arbiter is modeled
by a unique component and the arbitration protocol is carried out by the be-
havior of this unique arbiter. In this paper, as we are intending a distributed
implementation of the bus allocation arbiter, no unique component is model-
ing the arbiter, but a set of local arbiters, each one associated to a component
whether it is a processor or a bus. These local arbiters ensure arbitration by
interacting with their peers. The set of local arbiters of the processors is, as the
processors, modeled by a set of BIP components {P1 , P2 , . . . , PN }. The set of
local arbiters associated to buses are also modeled by a set of BIP components
{B1 , B2 , . . . , BM } (see Figure 3). In our model, we do not explicitly model the
dierent buses and processors as they are passive devices controlled each by a
local arbiter. Thus, we only give the description of the dierent arbiters.
Arbitration protocols are then achieved by the interaction between the dier-
ent arbiters. As already described in Section 2, interaction between components
in BIP can be described in a compact manner by connectors (see Denition 3).
In our model we describe how three well-known arbitration protocols could be
modeled using a set of structured connectors.

Fig. 3. A Distributed Model for multiple-bus architecture.

Our model contains N local arbiters associated each to a processor and M
local arbiters associated each to a bus. For the sake of readability, we limit the
gures describing our models to 3 processor arbiters namely {P1 , P2 , P3 } and 2
bus arbiters namely B1 and B2 (see Figure 3). Note that, such a model can be
easily extended to N and M arbiters (See Section 4).
Arbitration protocols are ensured by interactions between arbiters which are
here the set of BIP components {P1 , P2 , P3 , B1 , B2 }. These interactions are en-
capsulated in a set of BIP connectors namely {γ1 , γ2 , γ3 , γ4 , {γij }i∈[1,3]
j∈[1,2]
}. In this
work we focus on three well-known arbitration protocols namely: Fixed priority,
Equal priority and Rotating priority protocols [2]. Figure 3 describes the over-
all structure of our model which is the same for the description of the dierent
protocols. Indeed, the dierence between the models of the dierent protocols
is only some minor changes on connector characteristics. In other words, the
behavior of components, and the structure of connectors are almost the same
for all protocols. Each protocol is coded using variables, guards and functions
associated to each connector (Denition 3). For this reason, we describe rst
the model, depicted in Figure 3, for the xed priority protocol. Then we explain
how it can be easily extended to model rotating and equal priority protocols.
We start by the description of the behavior of the dierent BIP components,
then we detail the set of connectors ensuring the bus arbitration protocol.
Figure 4 describes the behavior and the set of ports of BIP components
modeling the processor arbiter Pi and the bus arbiter Bj . The two components
have 3 states namely q0 , q1 and q2 , where q0 is the initial state. The dierent
Fig. 4. Processor and Bus Arbiters.

transitions of the arbiters are labeled by one of their ports. These ports dene
how arbiters interact with the rest of components. The variables associated to
these ports can be read and updated through connectors. The behavior of the
processor arbiter can be described as follows:
Initially in state q0 , Pi can make a request by ring the transition labeled by
the port requestPi . As this port is a trigger port, Pi can re this transition
with no need to synchronize with any other components.
In q1 , two transitions are possible. If no bus is allocated, then Pi will re con-
tinuously a loop transition requestPi until a grantPi transition is performed.
This transition labeled by grantPi is red when Pi gets a bus access. If it
is the case, Pi goes to state q2 . As grantPi is a synchron port, ring the
corresponding transition depends on other conditions dened by the connec-
tors connecting this port. These conditions will be detailed at the level of
connectors description.
In state q2 , Pi has already a bus access. It can stay in this state as much
as it needs the bus. Once it decides to release it, the transition labeled by
releasePi is then red.

Figure 4 describes also the BIP component Bj of a bus arbiter. This arbiter
is quite a passive arbiter, as the protocol policy is ensured by BIP connectors.
Indeed, the bus arbiter receives the order to be assigned to a given processor
through its grantBj port. It, then receives the order to be released through its
releaseBj port. Details about how these orders are computed and sent are given
in the description of connectors.

Fixed-Priority Protocol In this section, a detailed description of each connec-
tor is given. We rst detail these connectors to model the xed priority protocol.
For the rest of protocols namely rotating and equal priority, we only give the up-
dates to perform on those connectors. In xed priority protocol, each processor
is assigned a xed and unique priority [5]. When more than M processors are re-
questing the bus at the same time, the M processors with the highest priority will
get a bus. The policy of this protocol is mainly ensured by connectors depicted in
Fig. 5. A Structured BIP connector modeling arbitration protocols.

Figure 3. The set of connectors γ1 ,γ2 and γ3 are detailed in Figure 5. The connec-
tor γ1 is a broadcast connector which connects 3 ports (requestPi , {i = 1, 2, 3}),
one of each processor arbiter. It describes the request procedure by the set of its
feasible interactions. In fact, as γ1 is a broadcast connector, the set of its feasible
interactions contains all possible subsets of its ports. The set of feasible inter-
actions of γ1 is {{requestP1 }, {requestP2 }, {requestP3 } , {requestP1 , requestP2 },
{requestP1 , requestP3 }, {requestP2 , requestP3 }, {requestP1 , requestP2 , requestP3 }}.
In the Upward function of γ1 , collects the identiers id and priorities pr of the
processors asking for a bus access. The values of these variables will be then
transferred to the exported port Ep1 , which exports this data to an upper con-
nector namely γ3 .
The Downward function of γ1 , allows Ep1 to send back, through the variable
nbus, the id of the allocated bus. If no bus is allocated to Pi , then the corre-
sponding nbus will be set to 0.

Notice that, for a given interaction, the temporary values of connector vari-
ables when executing the down instructions are computed by the corresponding
up instructions. However, these values are not accessible between dierent exe-
cutions of the same interaction or between the execution of the transfer functions
of dierent interactions. They are only stored between the execution of up and
down instructions of the same interaction. In the other words, the temporary
stored value is only accessible during the associated interaction and it will be
lost when the interaction is achieved. This means that connectors are memory-
less and no data can be stored at the connector level. This is a very interesting
aspect which makes our model indeed distributed because connectors are com-
pletely dierent from components and they do not have static variables. On the
other side, such a characteristic of connectors does not allow as to keep some
information like the id of asking and not served processors. For this reason, we
have modeled a loop transition labeled by the port requestPi which will be red
if no bus is allocated to Pi . In this way, the identiers id and priorities pr of
processors asking for a bus access can be collected again through the γ1 connec-
tor at the level of the upward function. The presence of such a loop transition
guarantees the no-blocking of our model after a rst allocation cycle of buses.
γ2 is connecting bus arbiters through the ports responseB1 and responseB2 .
By the means of its upward function, γ2 exports to port Ep2 the id of the avail-
able buses. The set of feasible interactions of γ2 is {{responseB1 }, {responseB2 },
{responseB1 , responseB2 }}.
The rendez-vous connector γ3 (see Figure 5), connects ports Ep1 and Ep2
which are respectively the exported ports of γ1 and γ2 . When the guard G =
(Ep1 · nb1 6= 0 ∨ Ep1 · nb2 6= 0 ∨ Ep1 · nb3 6= 0) ∧ (Ep2 · nc1 6= 0 ∨ Ep2 · nc2 6= 0)
is provided, the interaction involving the ports Ep1 and Ep2 occurs. The guard
G consists that at least there is one free bus and one processor which asks for
the access to a bus.
This connector implements with its upward function, called the DECIS al-
gorithm (see Algorithm 1), the protocol policy to manage the allocation of buses.
At the level of Ep1 , the id and priorities pr of the processors requesting a bus
are stored and at the level of Ep2 , variables save the id of available buses. Thus,
at the level of the exported port Exp of γ3 , all data needed to ensure the arbi-
tration protocol is available.
Our proposed DECIS algorithm consists in the selection of free buses as well
as processors asking for the bus access, then according to the order of priority
dened between processors the decision of the winners will be established. In-
deed, the proposed algorithm consists in the following steps:
1. Create an array of structure named P roc which has two members: id (iden-
tier) and pr (priority). P roc contains only the parameters of processors
asking for the bus access.
2. Create an array named Bus which contains only the identiers of free buses.
3. Call the function SORT that performs the sort of P roc according to the
priority pr.
4. Assign for each free bus the identier of the winner processor and for each
processor the identier of the allocated bus.
Algorithm 1 DECIS: For N processors and M buses
Require: interaction {Ep1 , Ep2 } if nc[i] 6= 0 then
Input: int nb[N ], P rio[N ], nc[M ] Bus[j] ← nc[i]
Output: int win[M ], nbg[N ] j ←j+1
j←1 end if
for i := 1; i <= N ; i + + do end for
if nb[i] 6= 0 and P rio[i] 6= 0 then l←j
P roc[j].id ← nb[i] SORT(P roc, k )
P roc[j].pr ← P rio[i] for i := 1; i <= l; i + + do
j ←j+1 idB ← Bus[i]
end if idP ← P roc[i].id
end for win[idB] ← idP
k←j nbg[idP ] ← idB
j←1 end for
for i := 1; i <= M ; i + + do

In the downward function of γ3 , the dierent variables are updated so that
each processor gets the id of the allocated bus (through port Ep1 ) and each
bus gets the id of the processor for which it was allocated (through port Ep2 ).
Notice that, if one decides to model a dierent protocol, the main modications
will be at the level of this connector.
As soon as, processors get the id of the allocated bus (through γ1 ) and buses
receive the id of the assigned processor (through γ2 ), transitions labeled by ports
grantPi and grantBi are red and the interaction Gi = {grantPi , grantBj } can
take place. This interaction is achieved through the γij connector (see Figure 6).

Fig. 6. Grant connector γij and Release connector γ4 .

Later, when a processor Pi decides to release a bus Bj , then the transition
releasePi is red and the interaction {releasePi , releaseBj } took place. This
interaction is performed through γ4 connector (see Figure 6).

Rotating-Priority Protocol In the rotating priority protocol, each device is
given a dierent priority in each arbitration cycle [5,14]. Which means that, if
a device has the highest priority in a rst cycle, it will have the lowest priority
in the next one, if it gets a bus. Priorities in this protocol are not static as
they are updated after every bus allocation. To model this protocol, we propose
to build upon the already described model. The idea is simply to add a new
port updatePi for each processor arbiter (see Figure 7). This port is connected
to grant port of each bus arbiter which allows to update the priority once a
bus allocation is performed (see Figure 7). The transition labeled by the port
updatePi is then possible in all processor states. Thanks to this new connector,
no changes in other existing connectors are needed as each priority variable pr
will always take the updated value.

Equal-Priority Protocol In the equal priority protocol, all devices have equal
priority of getting a bus upon request. When the number of requests is less or
equal to the number of free buses, all requests will be granted. If the number of
requests is higher than the number of free buses, then the choice of the winners
depends in general on the priority assigned to processors. However, when no
priority is dened between processors, which is the case of the equal priority
protocol, any conicts between requests to the buses will be solved at the level
of the BIP engine using the FIFO (First In Fist Out) rule. In fact, to model
the equal priority protocol, we use the same structure as the BIP model of the
Fig. 7. Processor behavior and Update Connector for Rotating priority protocol.

xed priority protocol with almost the same behavior and some modications
explained as follow:
When the conict between requests to the buses is managed using FIFO
rule, there is no need to implement the DECIS algorithm(see Algorithm 1)
for this protocol. Then, no data transfer is needed at the level of the struc-
tured connector (see Figure 5), thus the upward and downward functions
of this connector are removed. This structured connector allows so only the
transfer of the requests of various processors to the available buses.

When no priority is dened between processors, the variable pr associated
to the port requestPi , dening priority for each processor, is removed.
At the level of the grant connector γij , the guard is removed and the following
aectations are added:

grantBj .ncomp ← grantPi .id ; grantPi .nbus ← grantBj .id

At the level of the behaviors of both the bus and the processor controllers,
the only modication is the elimination of the guards of the grant transitions.

4 Implementation and Experimental Results

We propose to use BIP tools to verify and analyze the dierent models proposed
previously. In particular, we use the DFinder tool [15] oered by BIP toolbox to
verify the property of deadlock freedom of the already described arbitration pro-
tocols. DFinder is a compositional verication tool for deadlock detection where
verication is applied only to high level models for checking safety properties
such as invariants and deadlock-freedom. Based on this tool, we have proven
the deadlock freedom of the already described BIP models of the dierent arbi-
tration protocols at this abstract level of our model and with no need to code
generation. This is very interesting in the case of studying new protocols, one
Protocols Equal Priority Fixed Priority Rotating Priority
Time(ms) 48 57 187

Table 1. Deadlock Verication Time.

can decide about deadlock freedom of any protocol at a high-level model and
thusWecanran
modify and adjust on
our experiments theaprotocol easily. with Intel(R) Core (TM)2 Duo
Linux machine
2.93GHz × 2 and 16GiB memory. Table 1, shows verication time taken by the
tool for analyzing and detecting deadlock for our model. The time is computed
for a model with 5 processors and 2 buses.

N × M (Nbr of interactions) 25×15 (754) 30×20 (1204) 75×25 (3754) 100×50 (10004)
Time(Second) 2.7 3.8 120.1 814.9

Table 2. Analyzing/Detecting Deadlocks for Equal Priority Protocol

Extending our model to any number of processors and buses could be easily
performed as the dierent BIP components (processors and buses) have the same
behavior. For instance, we measure, in Table 2, the verication time for the
equal priority model for systems with more important number of components.
Extending easily the model to an important number of processors and buses
provides a way to study how protocols may react in the context of more complex
architectures and thus with more conicts to manage. Notice that increasing the
number of components increase consequently the number of conicts interactions
and so require more a more important time of exploration to detect deadlocks
and more memory resources.
Equal-Priority Fixed-Priority Rotating-Priority
k × 102
P1 P2 P3 P4 P5 P1 P2 P3 P4 P5 P1 P2 P3 P4 P5
1 22 21 20 18 19 47 50 0 0 0 19 20 21 22 18
10 196 215 192 191 206 491 506 0 0 0 198 201 202 203 196
100 2013 1997 2007 1990 1993 4912 5085 0 0 0 1997 2002 2005 1994 2002

Table 3. Model Based on Connectors: Number of grants per processor (k × 10 total
2

requests)

Once a model is proven to be deadlock free, further performance analysis
could be provided based on the code generated from BIP models. We now
give some experimental results obtained through this automatically generated
code to study fairness property of the dierent protocols. Indeed, fairness is a
key property one it comes to allocation protocols [16]. Ensuring fairness by a
protocol means that all processors will eventually get a bus if they ask for it.
Table 3 gives the number of times a processor gets the access to a bus for an
architecture of 5 processors and 2 buses.
In the case of the Fixed priority protocols we suppose that priorities are dened
as follows: P5 < P4 < P3 < P2 < P1 . As expected, the xed priority protocol
does not ensure fairness. The processors with the lower priorities (in this case P3 ,
P4 and P5 ) never get a bus access, if the rest of processors with higher priorities
ask for a bus. For this reason, the total of grants of dierent processors is equal
to the number of requests minus three, that is the three requests of the three
processors with the lower priorities whose never get a bus access.
The equal and the rotating priority protocols indeed ensure fairness as all
processors get an access to a bus in almost the same proportion. The equal
priority protocol is not always expected to ensure fairness as it depends on the
implementation of the required arbitration mechanism. If it implements fair
choice then fairness is guaranteed by the protocol. Notice that, in the results
presented in Table 3, our equal priority model is fair. This is expected as, in
the absence of specied priorities, the mechanism implemented in BIP treats re-
quests in a FIFO order. This means that any processor that have made a request
will eventually get a bus access. We propose also to check the mutual exclusion
on bus access for an architecture of 3 processors and 2 buses. The scenario where
two or more processors get access to the same bus at the same time can never
take place. Indeed, in our model depicted in Figure 5 the grant port of each bus
component {Bj }j∈{1,2} is connected to three dierent rendez-vous connectors
{γ1j , γ2j , γ3j }j∈{1,2} . According to BIP semantics [17], it is impossible to re
two synchronization involving common ports. This ensures that a bus can be
granted for one processor at a time.
The use of BIP is also highly motivated by the fact that BIP tools [18] oer an
automatically generated distributed code. Thus, once a model is proven to be
deadlock free or a set of relevant properties have been analyzed (such as fairness),
further performance analysis could be provided based on the code generated [19].

5 Related Work

Previous researches as in [4,2,3] have been interested by the design of arbitration
protocols for multiple-bus architecture. To analyze, evaluate and compare the
performance of dierent arbitration protocols, they have based only on estima-
tion (probabilistic models [4,3] and analytical models [2]). Thus, the obtained
results remain rough and thus not safe because they are based only on simula-
tions. As the choice of the adequate arbitration protocol is critical and has a
direct eect on the performance of the system, we thus need a powerful method
which provides correct and fully reliable results. For this reason, we have opted
for formal methods which are a particular kind of mathematically based tech-
niques for the specication, development and verication of systems. The use of
formal methods for system design provides reliability, correctness and robustness
of a design. In our research, we choose to describe the multiple bus architec-
ture using a component based framework BIP (see Section 2) which provides
correctness by construction and tools for formal verication of systems proper-
ties [7,19]. We were able to design a formal model which species in an elegant
way the multiple bus system for three priority schemes (equal priority, xed
priority and rotating priority). The major advantage of our model is that it is
almost the same for the three policies with minor changes at the level of the pro-
posed algorithm which manages conicts between concurrent processors. Unlike
the previous works that propose a distinct model for each arbitration proto-
col. Moreover, we have performed a formal validation of our model by verifying
deadlock freedom. We have also veried the fairness property for each protocol
which allows to compare the performance of dierent policies and so decide the
most adequate for multiple bus system. In [9], a formal model have been also
proposed using the BIP framework but only for a single bus architecture which
makes conict management completely dierent from our case. Moreover, in
multiple-bus architecture the distributed issue is more relevant than in [9]. Note
that in the dierent previously preformed researches, the proposed models are
only used for analysis and performance comparison and no code generation is of-
fered. Unlike ours, which in addition to formal validation, provides a distributed
automatically generated code [20].

6 Conclusion

We have proposed a high-level formal and abstract model for multiple-bus mul-
tiprocessors architecture. The proposed model provides a way for describing
dierent arbitration protocols in a distributed and abstract manner, which al-
lows to easily analyze and verify their dierent properties without having to
implement them in a concrete system. Indeed, in this paper we have proposed
several models for three well-known protocols namely, equal priority, xed prior-
ity and rotating priority. We have also performed several property verication of
the studied protocols and derived a distributed implementation of the proposed
models. Then experimental results have been provided using the dierent tools
provided by the BIP framework. Dierent new protocols could be also easily
described using the same principle, in particular if it is based on the same mul-
tiple bus architecture. As future work, we are considering to model new SoC
communication architectures as crossbar architecture [21] and thus to study and
verify its corresponding arbitration protocols as Round-Robin Protocol [22] and
Time Division Multiple Access (TDMA) [23].

References

1. N.Doifode, D., Dr.P.R.Bajaj: Design and performance analysis of ecient bus ar-
bitration schemes for on-chip shared bus multi-processor soc. International Journal
of computer Science and Network Security (IJCSNS) 8(9) (2008)
2. C.-M. Chung, D.A.C., Q.Yang: A comparative analysis of dierent arbitration
protocols for multiprocessors. Journal of Computer Science and Technology 11(3)
(1996)
3. John, L.K., Liu, Y.: Performance model for a prioritized multiple-bus multipro-
cessor system. IEEE Trans. Computers 45(5) (1996) 580588
4. Yang, Q., Raja, R.: Design and analysis of multiple-bus arbiters with dierent
priority schemes. In: Parallel Architectures (Postconference PARBASE-90). (1990)
276295
5. El-Guibaly, F.: Design and analysis of arbitration protocols. IEEE Trans. Comput.
38 (1989) 161171
6. J.-P. hilippe Fassino, J.-B Stefani, J.L., Muller, G.: Think: A software framework
for component-based operating system kernels. 16th IEEE Real Time Systems
Symposium (2002)
7. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in
bip. In: SEFM, IEEE Computer Society (2006) 312
8. Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-
Vincentelli, A.L.: Metropolis: An integrated electronic system design environment.
IEEE Computer 36(4) (2003) 4552
9. I.Ben-Hafaiedh, S., M.Jaber: Model-based design and distributed implementation
of bus arbiter for multiprocessors, IEEE ICECS (2011) 6568
10. Graf, S., Quinton, S.: Contracts for BIP: hierarchical interaction models for com-
positional verication. In: Proc. of FORTE'07. Volume 4574 of LNCS. (2007)
118
11. Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in bip.
IEEE Trans. Computers 57(10) (2008)
12. Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for
performance optimization in BIP. In: Proc. of SIES'09. (2009) 152160
13. Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed semantics and im-
plementation for systems with interaction and priority. In: Proc. of FORTE'08.
(2008) 116133
14. Kulmala, A., Salminen, E., Hamalainen, T.: Distributed bus arbitration algorithm
comparison on fpga based mpeg-4 multiprocessor soc. In: Norchip Conference,
2006. 24th. (nov. 2006) 167 170
15. S.Bensalem, M.Bozga, P.H.N., J.Sifakis: D-nder: A tool for compositional dead-
lock detection and verication. In: Computer Aided Verication. (2009) 614
619
16. Taub, D.: Arbitration and control acquisition in the proposed ieee 896 futurebus.
IEEE Micro 4 (1984) 2841
17. Bliudze, S., Sifakis, J.: Algebraic semantics of hierarchical connectors in the BIP
framework. Techreport, verimag (February 2007)
18. Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for
automated distributed implementation of component-based models. Distributed
Computing 25 (2012) 383409
19. Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.:
Formal verication of innite-state BIP models. In: Automated Technology for
Verication and Analysis - 13th International Symposium, ATVA 2015, Shanghai,
China, October 12-15, 2015, Proceedings. (2015) 326343
20. Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for
performance optimization in bip. In: SIES, IEEE (2009) 152160
21. S.Murali, L., Micheli, G.: An application-specic design methodology for on-chip
crossbar generation. Computer-Aided Design of Integrated Circuits and Systems
26(7) (2007) 12831296
22. E.S.Shin, V.J. Mooney, G.: Round robin arbiter design and generation, Interna-
tional Symposium on system synthesis (2002)
23. K. Lahiri, A. Raghunathan, G.L.: Lotterybus: A new high performance commu-
nication architecture for system-onchip designs, Design Automation Conference
(2001) 1520