Serge Haddad

Didier Lime

Olivier H Roux

A Turn-Based Approach for Qualitative Time Concurrent Games

We address concurrent games with a qualitative notion of time with parity objectives. This setting allows to express how potential controllers interact with their environment and more specifically includes relevant features: transient states where the environment will eventually act, controller avoiding of an environment action either by an immediate controller action or by masking it, etc. In order to solve the controller synthesis in this framework, we design a linear-time building of a timeless turn-based game and show a close connection between strategies of the controller in the two games. Thus we reduce the synthesis problem to a standard problem of turn-based game with parity objectives establishing as a side effect that pure memoryless strategies are enough for winning. Moreover we introduce permissiveness for safety and reachability games as a criterion to choose between winning strategies and prove that one can compute a most permissive strategy (when it exists) in linear time. Scan chain Convert CH3 Convert CH5 Inject CH2 Convert CH2 Convert CH5 Convert CH6 Inject CH1 Convert CH1 Convert CH6 Inject

Introduction

Games and controller synthesis. Finite games on graphs [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF] are widely recognized as an adequate formalism to address problems such as controller synthesis on discrete event systems, originally expressed and studied within the theory of supervision [START_REF] Wonham | On the supremal controllable sublanguage of a given language[END_REF][START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Golaszewski | Control of discrete event processes with forced events[END_REF]. The control problem can indeed be expressed as a game between two players representing respectively the controller and the environment. A controller for the system can be synthesized as a winning strategy for the controller player, when it exists. Real-time controller synthesis. For real-time systems, a strict turned-based game is an unnatural model, since the controller and the environment may play concurrently leading to concurrent games [START_REF] Chatterjee | Strategy improvement for concurrent reachability and safety games[END_REF][START_REF] Alfaro | Symbolic algorithms for infinitestate games[END_REF][START_REF] De Alfaro | Concurrent reachability games[END_REF]. Adding quantitative delays before playing actions is a way to select which action should be played. This results in formalisms called (concurrent) timed games [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]6], for which tools like UPPAAL-Tiga are available [START_REF] Behrmann | UPPAAL-Tiga: Time for playing games! In CAV[END_REF]. Nevertheless, the algorithmics of timed games is costly, and for instance, the mere existence of a controller is an EXPTIMEcomplete problem [START_REF] Jurdzinski | Reachability-time games on timed automata[END_REF] and the resulting strategies can be very large [START_REF] Ashok | SOS: Safe, optimal and small strategies for hybrid Markov decision processes[END_REF]. Furthermore from a modelling point of view, often the exact timing constraints are unknown and indeed not needed to ensure the existence of a winning strategy. Qualitative time concurrent games. To overcome these issues the authors of [START_REF] Béchennec | Control of DES with urgency, avoidability and ineluctability[END_REF][START_REF] Béchennec | Logical Time Control of concurrent DES[END_REF] have introduced a model of qualitative time concurrent game with the following features: actions of the environment may occur immediately or require some non null unknown delay and transient states where when the controller chooses not to (or cannot) play, an action of the environment is guaranteed to eventually occur. Then they have designed polynomial time (ad-hoc) algorithms synthesising (when it exists) a controller for reachability and safety goals. Our contribution. Our contribution is threefold. First we extend the model of [START_REF] Béchennec | Control of DES with urgency, avoidability and ineluctability[END_REF] by allowing some actions of the environment to be blocked by the controller and considering parity objectives. Then we design a linear-time building of a timeless turn-based game and show a close (but not one-to-one) connection between strategies of the controller in the two games. Thus we reduce the synthesis problem to a standard problem of turn-based game with parity objectives establishing as a side effect that pure memoryless strategies are enough for winning. Finally we introduce permissiveness for safety and reachability games as a criterion to choose between winning strategies and prove that one can compute a most permissive strategy (when it exists) in linear time. Organisation. We illustrate by a relevant example the interest of our framework in Section 2. Section 3 gives the basic definitions and terminology used in this paper. Section 4 provides the translation to turn-based games and establishes the connections between strategies. Section 5 introduces the notion of permissiveness and shows how to compute most permissive strategies. Finally, we conclude in section 6.

A motivating example

A device driver is the interface between the hardware device and the application or the operating system. Being executed with supervisor privileges, any error in a driver may have a serious impact on the integrity of the entire system. A specific driver (as opposed to a generic driver) is a driver dedicated to an application, i.e., with a smaller memory footprint.

In the context of driver synthesis, the environment is both the hardware device and the application using the driver. Then uncontrollable actions are interrupts that are triggered by the hardware and the requests made by the application.

Let us consider an analog-to-digital converter (ADC) inspired by the one of the MPC5xx microcontrollers family. An ADC cell has multiplexed acquisition channels (only one channel at a time). In order to allow the conversion of several channels, the conversions are combined into a conversion chain.

There are two types of conversion: normal or injected. In a normal conversion, it is possible to make a chain of conversion uniquely (oneShot) or continuously (scan). In oneShot mode, the cell stops acquisition at the end of the conversion, while in scan mode it repeats the chain ad infinitum (until a stop action is performed).

If one wants to make a oneShot acquisition in the middle of a conversion in scan mode, it is possible to use the injected conversions. An injected conversion is analogous to a software interrupt (inject) that can be maskable, i.e., it can be disabled. When an injected conversion is started, any conversion in progress is interrupted. The injected conversion is then carried out. At the end of the injected conversion, the chain which was interrupted resumes where it had been stopped (see Figure 1 for channel CH5). If a conversion is interrupted twice by two injected conversions, then it is lost and the scan goes to the next one (see Figure 1 for channel CH6). Fig. 1: Conversion chain Scan for channels 3,5,6,8 with some injected conversions.

A conversion takes a non-null time that is not known precisely. At the end of a conversion the hardware generates an interrupt EOC (end of conversion). This interruption is ineluctable, i.e., it is guaranteed to happen eventually.

Finally, the converter can sleep or be awake but if a conversion request occurs while sleeping, the driver must return an error to the application. Let us take stock of what we need to model:

controllable actions of the driver uncontrollable actions of the environment where:

• some uncontrollable actions take a non-null time and cannot happen immediately (oneShot, scan, eoc); • some uncontrollable actions are guaranteed to happen eventually. The input state of such a transition is then a transient state (oneShot, scan, eoc); • some uncontrollable actions are maskable (inject): they can be disabled by the controller.

Definitions

The following definitions introduce a kind of concurrent game between the controller (denoted by C) and the environment (denoted by U ). In all states q ∈ Q, C (resp. U ) selects an action in Avail C (q) ⊆ A C (resp. Avail U (q) ⊆ A U ). As seen in Definition 2, it selects a qualitative delay for performing its action and it can block a subset of the maskable actions of the environment (A m U ). C may also be inactive while the environment has to act in transient states (QT ). Thus in all q ∈ QT , an unmaskable action is available, i.e. Avail U (q) \ A m U ̸ = ∅.

Definition 1 (Game structure). A game structure is a tuple G = (Q, A C , Avail C , A U , Avail U , δ) where:

-Q = QT ⊎ QI is a set of states partitioned in transient states QT and idle states QI with q 0 ∈ Q, the initial state;

-A C is the set of actions of the controller and Avail C : Q → 2 A C defines its available actions depending on states. -A U is the set of actions of the environment with A C ∩ A U = ∅ and Avail U : Q → 2 A U defines its available actions depending on states. A U includes the set of avoidable actions A a U and the set of maskable actions

A m U . -δ : Q × A C ∪ A U → Q is the transition function such that δ(q, a) is defined if
and only if a ∈ Avail C (q) ∪ Avail U (q). For all q ∈ QT , Avail U (q) \ A m U ̸ = ∅. Given a current state q, the controller decides whether it intends to act (0 or 0) or not (ε), which action it intends to perform, when it will act (immediately: 0; or later: 0) and which actions it will block.

Definition 2 (Decision).

Let G be a game structure and q ∈ Q. Then the set of decisions of the controller Dec(q) is defined as follows. (γ, τ, B) ∈ Dec(q) if:

the action γ ∈ Avail C (q) ∪ {ε} where ε denotes inaction; the delay τ ∈ {0, 0, ε} fulfills τ = ε iff γ = ε; the actions to be masked

B ⊆ A m U ∩ Avail U (q).
Given a state q and a decision d of the controller, the next state to be reached may be either (1) q itself if it is idle and the controller is inactive, either (2) the state reached by the action selected by the controller (if any), or (3) a state reached by an environment action that has not be preempted by the action of the controller played without delay or masked by the controller. Definition 3 (Play transitions). Let G be a game structure, q ∈ Q and d = (γ, τ, B) ∈ Dec(q), the set of play transitions Next(q, d) is defined by:

-If γ = ε and q ∈ QI then q d,ε = = ⇒ q ∈ Next(q, d);

-If γ ̸ = ε then q d,γ = = ⇒ δ(q, γ) ∈ Next(q, d); -For all a ∈ Avail U (q) \ (A a U ∪ B), q d,a = = ⇒ δ(q, a) ∈ Next(q, d); -If τ ̸ = 0 then for all a ∈ Avail U (q) ∩ A a U \ B, q d,a = = ⇒ δ(q, a) ∈ Next(q, d). By construction, Next(q, d) is never empty: if γ ̸ = ε then q d,γ = = ⇒ δ(q, γ) ∈ Next(q, d) else if q ∈ QI then q d,ε = = ⇒ q ∈ Next(q, d) else there is some a ∈ Avail U (q) \ A m U such that q d,a = = ⇒ δ(q, a) ∈ Next(q, d).
A play is a finite or infinite sequence of play transitions such that the source of a non initial transition is the destination of the transition that precedes it. Definition 4 (Play). Let G be a game structure. Then r = (q n dn,an

= === ⇒ q n+1 ) n∈N
where for all n ∈ N, d n ∈ Dec(q n ) and q n dn,an

= === ⇒ q n+1 ∈ Next(q n , d n ) is an infinite play.
A finite play r is a finite prefix of an infinite play, ending in a state denoted Last(r). R (resp. R) denotes the set of infinite (resp. finite) plays. The empty play is denoted by λ with Last(λ) = q 0 . A strategy of the controller restricts the underlying transition system of the concurrent game by selecting a decision for all finite plays allowed by the strategy. Thus this mapping is inductively defined, simultaneously with its domain.

Definition 5 (Strategy)

. A controller strategy s C is a partial mapping from R to q∈Q Dec(q) with its domain denoted Dom(s C ) inductively defined by:

λ ∈ Dom(s C );

for all r ∈ Dom(s C ), s C (r) ∈ Dec(Last(r)) and for all Last(r)

s C (r),a = ==== ⇒ q ∈ Next(Last(r), s C (r)), r(Last(r) s C (r),a = ==== ⇒ q) ∈ Dom(s C ).
A play r = (q n dn,an

= === ⇒ q n+1 ) n∈N complies with s C if for all n, d n = s C ((q m dm,am = ==== ⇒ q m+1 ) m<n ). The outcome of s C , denoted by Outcome(s C ), is the set of infinite plays complying with it.
Any decision of a positional (also called memoryless) strategy s C only depends on the last state of the play. For such a strategy, given some q ∈ Q, s C (q) denotes the decision of s C for any finite play with last state q.

A goal W for the controller is a subset of Q ω . W.r.t. W , a strategy s C is winning for q 0 if for all plays (q n dn,an

= === ⇒ q n+1 ) n∈N complying with s C , (q n ) n∈N ∈ W . A parity goal W µ is defined by a mapping µ from Q to N. Let s = (q n ) n∈N define m µ (s) = max(i | ∀n ∃n ′ ≥ n i = µ(q n ′ )). Then s ∈ W µ iff m µ (s) is even.
Parity goals include several kinds of goals like safety and reachability goals. A game is a pair (G, W ).

From concurrent games to turn-based games

A turn-based game interpretation. In order to apply the theory and algorithms of parity turn-based games, we propose below a linear-time translation of a concurrent game structure G into a turn-based one G such that given some parity goal W : (1) the controller has a winning strategy for (G, W ) iff it has a winning strategy ( G, W ) and ( 2) from a positional winning strategy in ( G, W ), one can build in linear time a positional winning strategy in (G, W ). Definition 6. G = ( Q, →), a turn-based game structure is defined by:

-

Q = Q C ⊎ Q U , the set of states with q 0 ∈ Q C , the initial state; -→⊂ Q × Q the transition relation fulfilling: ∀q ∈ Q ∃q ′ ∈ Q q → q ′ .
We denote Own the mapping from Q to {C, U } defined for all q ∈ Q by

Own(q) = C if and only if q ∈ Q C . (q n ) n∈N ∈ Q ω is an infinite play of G if for all n ∈ N, q n → q n+1 . A sequence (q m ) m≤n ∈ Q * Q C is a finite play if for all m < n, q m → q m+1
. Note that we only define finite plays ending in states owned by C, as only those will be useful to define strategies for C.

Definition 7 (Strategy).

A strategy s C of G is a partial mapping from the set of of finite plays to Q with its domain denoted Dom(s C ) inductively defined by:

-q 0 ∈ Dom(s C ); -for all ρ = (q m ) m≤n ∈ Dom(s C ), s C (ρ) ∈ Q with q n → s C (ρ) and for all ρ ′′ = ρs C (ρ)ρ ′ , such that s C (ρ)ρ ′ ∈ Q * U Q C ρ ′′ ∈ Dom(s C ). A play ρ = (q n ) n∈N complies with s C if for all n, such that q n ∈ Q C , q n+1 = s C ((q m ) m≤n ). The outcome of s C , denoted Outcome(s C ), is the set of infinite plays complying with it. Let W ⊆ Q ω be a goal, s C is winning in ( G, W ), if Outcome(s C ) ⊆ W .
In order to obtain a canonical translation we assume an enumeration order of A C and A U . It should be be clear that the results hold whatever the chosen order. According to this order, define for all q ∈ Q:

maskable uncontrollable actions:

Avail U (q) ∩ A m U = {α q 1 , . . . , α q ℓq }; unavoidable maskable uncontrollable actions:

(Avail U (q) ∩ A m U ) \ A a U = {α q 1 , . . . , α q kq } with k q ≤ ℓ q ; unmaskable uncontrollable actions:

Avail U (q) \ A m U = {β q 1 , . . . , β q nq };

unavoidable unmaskable uncontrollable actions:

Avail U (q) \ (A a U ∪ A m U ) = {β q 1 , .
. . , β q mq } with m q ≤ n q ; controllable actions:

Avail C (q) = {γ q 1 , . . . , γ q pq }.

In order to avoid handling particular cases, Definition 8 assumes that for all q, k q ≥ 1, n q ≥ 1, and p q ≥ 1. Afterwards, we explain how to adapt the translation when this is not the case. Let us first informally describe how the turn-based version G of game G is specified:

-The states of G are also states of G and belong to the controller. In such a state q, the controller has three choices (see Figure 3):

• either it decides to (try to) play immediately going to state (q C 0 , α q 1 ); • either it decides to (try to) play not immediately going to state (q C 0 , α q 1 ); • or it decides to be inactive, going to state (q C ε , α q 1 ).

q (q C 0 , α q 1 ) (q C 0 , α q 1 ) (q C ε , α q 1 )
Fig. 3 -From state (q C 0 , α q 1 ), the controller successively either lets the environment the availability of action α q 1 by going to (q U ε , α q 1 ) or masks this action by going to (q C 0 , α q 2 ). After all maskable unavoidable actions have been enumerated (and masked or not played), in q U 0 the environment can play any unavoidable and unmaskable action or, by going in q C 0 , let the controller play an action (see Figure 4).

-The situation from state (q C 0 , α q 1 ) is similar to the previous one except that the controller first enumerates all the maskable actions and in q U 0 the environment can play any unmaskable action (see Figure 5).

-The situation from state (q C ε , α q 1 ) is similar to the previous one except that in q U ε , if q is transient the environment must play some unmaskable action while if q is idle it can decide to be inactive going back to q (see Figure 6).

(q C 0 , α q ) (q U 0 , α q 1 ) (q C 0 , α q 2 ) (q C 0 , α q kq ) (q U 0 , α q kq ) q U 0 δ(q, α q 1 ) δ(q, α q kq ) q C 0 δ(q, β q 1 )
δ(q, β q mq ) δ(q, γ q 1 ) δ(q, γ q pq ) . . . . . . . . .

Fig. 4

(q C 0 , α q 1 ) (q U 0 , α q 1 ) (q C 0 , α q 2 ) (q 0 , α q ℓq ) (q U 0 , α q ℓq ) q U 0 δ(q, α q 1 ) δ(q, α q ℓq ) q C 0 δ(q, β q 1 )
δ(q, β q nq ) δ(q, γ q 1 ) δ(q, γ q pq ) . . . . . . . . .

Fig. 5

Definition 8. Let G be a game structure. Then G = ( Q, Own, →), a turn-based game structure, is defined as follows:

-Q = Q ∪ {q y x | q ∈ Q ∧ ((x ∈ {0, 0} ∧ y ∈ {C, U }) ∨ (x = ε ∧ y = U ))} ∪ {(q y x , α q i )) | q ∈ Q∧y ∈ {C, U }∧(x = 0∧(i ≤ k q ))∨(x ∈ {0, ε}∧(i ≤ ℓ q ))}; -Q C = Q ∪ {q C x } q,x ∪ {(q C x , z)} q,x,z , Q U = Q ∪ {q U x } q,x ∪ {(q U
x , z)} q,x,z ; -→ is defined by for all q ∈ Q and all x ∈ {0, 0, ε}, q → (q C

x , α q 1 ) and: Case of immediate play controller choice.

• For all q and i ≤ k q , (q C 0 , α q i ) → (q U 0 , α q i ) and (q U 0 , α q i ) → δ(q, α q i );

C ε , α q 1 ) (q U ε , α q 1 ) (q C ε , α q 2 ) (q C ε , α q ℓq ) (q U ε , α q ℓq ) q U ε δ(q, α q 1 ) δ(q, α q ℓq ) q δ(q, β q 1 )
δ(q, β q nq ) . . . . . . when q is idle Fig. 6 • For all q and i < k q , (q C 0 , α q i ) → (q C 0 , α q i+1 ) and (q U 0 , α q i ) → (q C 0 , α q i+1 ); • For all q, (q C 0 , α q kq ) → q U 0 and (q U 0 , α q kq ) → q U 0 ; • For all q and i ≤ m q , q U 0 → δ(q, β q i ) and q U 0 → q C 0 ; • For all q and i ≤ p q , q C 0 → δ(q, γ q i ). Other Cases (x ∈ {0, ε}).

• For all q and i ≤ ℓ q , (q C x , α q i ) → (q U x , α q i ) and (q U x , α q i ) → δ(q, α q i ); • For all q and i < ℓ q , (q C

x , α q i ) → (q C x , α q i+1 ) and (q U x , α q i ) → (q C x , α q i+1 ); • For all q, (q C

x , α q ℓq ) → q U x and (q U x , α q ℓq ) → q U x ; • For all q and i ≤ n q , q U

x → δ(q, β q i ); • q U 0 → q C 0 and for all q ∈ Q and i ≤ p q , q C 0 → δ(q, γ q i ); • When q ∈ QI, q U ε → q.

Let us explain how to address the particular cases. For instance when ℓ q =0, the three transitions outgoing from q target the states q U 0 , q U 0 and q U ε . The other particular cases are similarly handled.

Example 2. Figure 7 partly illustrates this translation for the game structure of Figure 2, starting from transient state q 0 . In all figures illustrating G, states owned by the controller are represented by circles while states owned by the environment are represented by rectangles.

Correspondence between plays. We want to establish a correspondence between plays of G and plays of G. With this aim, we introduce connecting paths of G. Definition 9. A connecting path of G is a path from some q ∈ Q to some q ′ ∈ Q that does not visit in between other states of Q.

Let ρ be a connecting path. We denote src(ρ) the source state of ρ and dst(ρ) its destination state. Given two connecting paths ρ, ρ ′ such that q, the target state of ρ, is the source state of ρ ′ , ρρ ′ denotes the concatenation of ρ and ρ ′ without the repetition of q. As usual, this operation is extended to finite or

Avail U (q0) \ A m = {oneShot, scan}
Avail C (q0) = {W akeup} kq 0 = 0, ℓq 0 = 0, mq 0 = 0, nq 0 = 2

β q 0 1 = β q 0 m+1 = oneShot β q 0 2 = β q 0 n = scan γ q 0 1 = W akeup δ(q0, β q 0 1 ) = δ(q0, β q 0
2 ) = qerr, δ(q0, γ

q 0 1 ) = q1 q0 q U 0 0 q C 0 0 qerr q 1 q U 0 0 q C 0 0 q U 0ε
Fig. 7: The controller choices from q 0 countable paths. Observe that any infinite play of G is a countable concatenation of connecting paths. The following lemma lists all possible connecting paths. We omit its proof as it straightforwardly comes from examination of the local structure of G. Observe that we associate an action with a connecting path.

Lemma 1. Let q ∈ Q. Then all connecting paths starting from q can be concisely specified (with an associated action a ρ ) as follows:

ρ(q, y, B, α q i ), the path that (1) starts from q to (q C y , α q 1 ), (2) goes to (q U y , α q i ) avoiding the set {(q U y , α q j ) | α q j ∈ B}, and (3) reaches δ(q, α q i ). a ρ = α q i ; ρ(q, y, B, β q i ), the path that (1) starts from q to (q C y , α q 1 ), (2) goes to q U y avoiding the set {(q U y , α q j ) | α q j ∈ B}, and (3) reaches δ(q, β q i ). a ρ = β q i ; ρ(q, y, B, γ q i ), the path that (1) starts from q to (q C y , α q 1 ), (2) goes to q C y avoiding the set {(q U y , α q j ) | α q j ∈ B}, and (3) reaches δ(q, γ q i ). a ρ = γ q i ; when q is idle, ρ(q, ε, B, ε), the path that (1) starts from q to (q C ε , α q 1 ), (2) goes to q U ε avoiding the set {(q U y , α q j ) | α q j ∈ B}, and (3) returns to q. a ρ = ε.

We now relate play transitions of G to connecting paths of G.

Definition 10. Let e = q d,a = = ⇒ q ′ with d = (γ, τ, B) be a play transition of G. Then the connecting path ê is defined as follows:

-If a = α q i for some α q i then ê = ρ(q, τ, B ′ , α q i ) with B ′ = {α q j | j < i} ∩ B; -If a = β q i for some β q i then ê = ρ(q, τ, B, β q i ) -If a = γ q i for some γ q i then ê = ρ(q, τ, B, γ q i ); -If a = ε then ê = ρ(q, τ, B, ε);

We now extend in a natural way the correspondence between transitions to plays.

Definition 11 (Relation between plays). Let r = (e n ) n≤N (resp. r = (e n ) n∈N ) be a finite (resp. infinite) play of G. Then r a finite (resp. infinite) play of G, is defined by r = (ê n ) n≤N (resp. r = (ê n ) n∈N ). between strategies. Let G be a concurrent game structure and ρ = (q n ) n∈N ∈ Q ω . Define π(ρ) as (q α(n) ) n∈N where α is a strictly increasing mapping from N to N with the range of α being {n | q n ∈ Q}. This means, π extracts the subsequence of states from the original game from any play in the turn-based game. Let W be a goal of G.

Then W ⊆ Q ω , a goal of G, is defined by W = {ρ | π(ρ) ∈ W }.
In order to obtain a correspondence between strategies, we focus on translating a decision d ∈ Dec(q) in G into a local positional strategy d of G. Given a state q and a decision d = (γ, τ, B) induced by a strategy in G, the 'local' corresponding strategy in G consists in allowing exactly the connecting paths ê such that e ∈ N ext(q, d). Thus, (1) in q the strategy selects (q C τ , α q 1 ), ( 2) in all states (q C τ , α q i ), it selects (q U τ , α q i ) if α q i / ∈ B and avoids it otherwise, and (3) when γ ̸ = ε, it selects in q C τ the state δ(q, γ). Definition 12 (From decisions to local strategies). Let q ∈ Q and d = (γ, τ, B) ∈ Dec(q). The partial mapping d : Q → Q is defined as follows:

d(q) = (q C τ , α q 1 ); for all (defined

) (q C τ , α q i ) if α q i / ∈ B then d(q C τ , α q i ) = (q U τ , α q i ); -for all (defined) (q C τ , α q i ) if α q i ∈ B and (i, τ ) / ∈ {(k q , 0), (ℓ q , 0), (ℓ q , ε)} then d(q C τ , α q i ) = (q C τ , α q i+1 ); -for all (defined) (q C τ , α q i ) if α q i ∈ B and (i, τ ) ∈ {(k q , 0), (ℓ q , 0), (ℓ q , ε)} then d(q C τ , α q i ) = q U τ ; -If γ ̸ = ε then d(q C
τ )) = δ(q, γ). Definition 13. Let d ∈ Dec(q). A connecting path ρ starting from q complies with d if for all transitions q 1 → q 2 of ρ with q 1 ∈ Q C , q 2 = d(q 1 ).

By examining all possible cases, one gets the following lemma.

Lemma 2. Let q ∈ Q and d = (γ, τ, B) ∈ Dec(q). Then:

N ext(q, d) = {q d,aρ
= == ⇒ dst(ρ) | ρ is a connecting path with src(ρ) = q complying with d} Example 3. Let us consider the example of Figure 2. Figure 8 shows the result of the decision d = (γ q2 1 , 0,

{α q2 1 }) = (N ext Sample, 0, {inject}) from q 2 . α q 2 1 = α q 2 k = inject β q 2 1 = β q 2 m = stop γ q 2 1 = N ext Sample δ(q 2 , β q 2 1 ) = q 1 δ(q 2 , γ q 2 1 ) = q 3 q2 q U 2 0 q C 2 0 q1 q3
Fig. 8: The connecting paths from q 2 complying with d = (N ext Sample, 0, {inject}) Given the decisions selected by a strategy s C of G and applying the corresponding local strategies, one gets a strategy ŝC of G. The next definition is sound since, by induction and using 2, for every finite play ρ that complies with ŝC and ends in Q, there is some r ρ that complies with s C such that ρ = r.

Let q ∈ Q, τ ∈ {0, 0, ε}, α ∈ A m U such that (q U τ , α) ∈ Q and B ⊆ A m U ∩ Avail U (q). Then (q U τ , α) ↓B denotes (q U τ , α) if α / ∈ B and the empty word of Q * otherwise.

Definition 14. Let s C be a controller strategy of G. Then ŝC , a controller strategy of G is defined by induction on the length of ρ = rρ where r ρ is a finite play of G complying with s C and ending in some q ∈ Q as follows when denoting s C (r) by d = (γ, τ, B).

-ŝC (ρ) = d(q); for all (defined) (q C τ , α q i ), ŝC (ρ(q C τ , α q 1 )(q U τ , α q 1 ) ↓B . . .

(q C τ , α q i )) = d(q C τ , α q i ) -If γ ̸ = ε then ŝC (ρ(q C τ , α q 1 )(q U τ , α q 1 ) ↓B . . . (q C τ , α q kq )(q U τ , α q kq ) ↓B q U τ q C τ )) = d(q C τ )
). Let ρ * = ρρ ′ where ρ ′ is a a connecting path complying with d and associated action a ρ ′ . Then

r ρ * = r ρ (Last(r ρ ) d,a ρ ′ ===⇒ dst(ρ ′ )).
Applying inductively Lemma 2, one immediately gets the next proposition and corollary: Proposition 1. Let s C be a controller strategy of G. Then:

Outcome(ŝ C ) = {r | r ∈ Outcome(s C )} Corollary 1.
Let Goal ⊆ Q ω be a goal and s C be a winning strategy for Goal in G. Then ŝC is a winning strategy for Goal in G.

In order to get the converse result we exploit the fact that positional strategies are sufficient for turn-based parity games.

Definition 15. Let s C be a positional controller strategy of G. Then s C is a positional controller strategy of G defined as follows. Let q ∈ Q and denote s C (q) = (γ, τ, B).

-

If s C (q) = (q C 0 , α q 1 ) and s C (q C 0 ) = δ(a, γ q i ) then γ = γ q i , τ = 0 and B = {i ≤ k q | s C ((q C 0 , α q i )) ̸ = (q U 0 , α q i )}; -If s C (q) = (q C 0 , α q 1 ) and s C (q C 0 ) = δ(a, γ q i ) then γ = γ q i , τ = 0 and B = {i ≤ ℓ q | s C ((q C 0 , α q i )) ̸ = (q U 0 , α q i )}; -If s C (q) = (q C ε , α q 1 ) then γ = ε, τ = ε and B = {i ≤ ℓ q | s C ((q C 0 , α q i )) ̸ = (q U 0 , α q i )};
Observe that s C (q) is an item of Dec(q), say d, and that s C restricted to the subset of states of Q related to q can be viewed as a local strategy, say d ′ . By construction, d ′ = d. Thus applying inductively Lemma 2, one immediately gets the next proposition and corollary:

Proposition 2. Let s C be a positional controller strategy of G. Then:

Outcome(s C ) = {r | r ∈ Outcome(s C )}.
2. Let Goal ⊂ Q ω be a parity goal and s C be a winning positional strategy for Goal in G. Then s C is a winning positional strategy for Goal in G.

Combining corollaries 1 and 2, one gets: Theorem 1. Let G be a concurrent game, Goal ⊆ Q ω be a parity goal.

-Let s C be a controller strategy. Then s C is a winning strategy for Goal if and only if ŝC is a winning strategy for Goal; -If there is a winning strategy for G, there is a positional one, i.e. s ′ C where s ′ C is any positional winning strategy of G.

Permissivity of the controller

Permissivity is a criterion that has to be taken into account for choosing between possible controllers. In our context and due to the results of the previous section, we limit ourselves to positional controllers. First we introduce an order between controller decisions. In words, a decision d ′ is more permissive than d if (1) either d ′ is inactive or intends to play the same action as d, (2) the delay before acting of d ′ is greater or equal than the delay before acting of d, and (3) the set of actions masked by d ′ is a subset of actions masked by d. Here permissivity should be interpreted as the controller avoiding to restrict the behaviour of the environment.

Definition 16. Let q be a state and d = (γ, τ, B) and d ′ = (γ ′ , τ, B) be two decisions, one says that d ′ is more (or equally) permissive than d denoted by

d ⪯ d ′ if: γ ′ = γ or γ ′ = ε, τ ≤ τ ′ and B ′ ⊆ B.
Assuming that there exists a winning strategy for q 0 , our goal is to define and synthesise a maximally permissive winning strategy for q 0 w.r.t. safety and reachability goals. As explained later we introduce slightly different notions of maximally permissive winning strategy depending on the kind of goal. Observe that in the next definition, we do not care about losing states of the game since winning strategies do not enter losing states.

Definition 17. Let s C and s ′ C be positional winning controller strategies of (G, Goal) where Goal is a safety goal. Then s ′ C is more permissive than s C w.r.t. Goal, denoted s C ⪯ s ′ C , if for all q winning state of (G, Goal), s C (q) ⪯ s ′ C (q). Additionally,

s C ≺ s ′ C if s C ⪯ s ′ C and s ′ C ⪯̸ s C . s C is a maximally permissive winning strategy w.r.t. Goal if there is no s ′ C such that s C ≺ s ′ C .
The synthesis of a maximally permissive winning strategy w.r.t. a safety goal is easy. Since it is enough to stay in the winning states, maximally permissive decisions can be combined without any restriction to get a maximally permissive winning strategy.

Theorem 2. Let G be a concurrent game and Goal be a safety goal. Once the winning states of ( G, Goal) have been computed, a maximally permissive winning strategy of (G, Goal) for q 0 can be computed in linear time.

Proof. We compute for all q, state of (G, Goal) (and thus of ( G, Goal)), a most permissive decision. Since we deal with a safety goal, any combination of decisions works. A maximally permissive decision for q is computed as follows.

-If (q C ε , α q 1 ) is winning then define B = {α q i | i ≤ ℓ q ∧ δ(q, α q i ) is not winning}. By construction, (ε, ε, B) is a maximally permissive decision; -If (q C ε , α q 1 ) is not winning and (q C 0 , α q 1 ) is winning then define B = {α q i | i ≤ ℓ q ∧ δ(q, α q i ) is not winning}. The set {γ q i | i ≤ p q ∧ δ(q, γ q i ) is winning} is not empty since (q C 0 , α q 1 ) is winning. Pick some γ q i inside. By construction, (γ q i , 0, B) is a maximally permissive decision; -If (q C ε , α q 1 ) and (q C 0 , α q 1 ) are not winning then (q C 0 , α q 1 ) is winning. Define B = {α q i | i ≤ k q ∧ δ(q, α q i ) is not winning}. The set {γ q i | i ≤ p q ∧ δ(q, γ q i ) is winning} is not empty since (q C 0 , α q 1 ) is winning. Pick some γ q i inside. By construction, (γ q i , 0, B) is a maximally permissive decision.

⊓ ⊔

The definition of a maximally permissive winning strategy w.r.t. a reachability goal is more involved since we want to take into account the delay before reaching the target state q f assumed w.l.o.g. to be absorbing (i.e., its only outgoing transition is a self-loop).

Definition 18. Let G be a concurrent game structure and Goal be a reachability goal defined by an absorbing target state q f . Let s C be a positional winning strategy and q ∈ Q be a winning state. Then delay s C (q), the delay of q ̸ = q f w.r.t. s C is defined by: delays C (q) = max(n | (qm dm,am = ==== ⇒ qm+1) 1≤m<n complying to sC , q = q1, ∀i qi ̸ = q f ) By convention, delay s C (q f ) = 0. The minimal delay of a q, denoted delay * (q) is defined by: delay * (q) = min(delay s C (q) | s C is a winning strategy)

We also restrict the constraint for maximality for decisions of a strategy s C to states visited by s C : a state q is visited by s C if there is a finite play complying to s C starting in q 0 and ending in q.

Definition 19. Let s C and s ′ C be positional winning controller strategies of (G, Goal) where Goal is a reachability goal defined by an absorbing target state q f . Then

s ′ C is more permissive than s C w.r.t. Goal, denoted s C ⪯ s ′ C , if for all q state visited by s C , s C (q) ⪯ s ′ C (q) and delay s ′ C (q) ≤ delay s C (q). s C ≺ s ′ C if s C ⪯ s ′ C and s ′ C ⪯̸ s C . s C is a maximally permissive winning strategy w.r.t. Goal if there is no s ′ C such that s C ≺ s ′ C .
Let us informally explain how the proof of the next theorem proceeds to synthesise a maximally permissive winning strategy. If q 0 = q f we are done. Otherwise define Q 0 = {q f } and Q 1 to be the set of states q ̸ = q f for which there is a decision d such that all the transitions of Next(q, d) lead to Q 0 . Observe that set is non empty. Otherwise q 0 could not be a winning state. For such q select d maximally permissive among these kinds of decisions. If q 0 ∈ Q 1 we are done. We iterate this process until q 0 is found. Assume Q 0 , . . . , Q i have been built with q 0 / ∈ j≤i Q j . Define Q i+1 to be the set of states q / ∈ j≤i Q j for which there is decision d such that all the transitions of Next(q, d) lead to j≤i Q j . Observe that this set is non empty. Otherwise q 0 could not be a winning state. For such q select d maximally permissive among these kinds of decisions. Since Q is finite this process must stop with q 0 belonging to some Q i * .

Theorem 3. Let G be a concurrent game structure and Goal be a reachability goal defined by an absorbing target state q f . Then a maximally permissive winning strategy of (G, Goal) for q 0 can be computed in linear time.

Proof. As explained we proceed by iteratively building disjoint sets of states Q 0 , Q 1 , . . . as long as q 0 does not belong to these states. Furthermore we associate decisions with every state belonging to these sets, that define the strategy s C . We set Q 0 = {q f } and since q f is absorbing, the associated decision is (ε, ε, ∅). Assume that Q 0 , Q 1 , . . . , Q i have been built with q 0 / ∈ j≤i Q j . For sake of readability, we write

Q ′ = j≤i Q j . Let q / ∈ Q ′ . -If q is transient and for all k ≤ n q , δ(q, β q k ) ∈ Q ′ then q ∈ Q i+1 and defining B = {α q k | k ≤ ℓ q ∧ δ(q, α q k ) / ∈ Q ′ }, (ε, ε, B
) is the decision associated with q; -Else if for all k ≤ n q , δ(q, β q k ) ∈ Q ′ and there exists γ q p such that δ(q, γ q p ) ∈ Q ′ then q ∈ Q i+1 and defining B = {α q k | k ≤ ℓ q ∧ δ(q, α q k ) / ∈ Q ′ }, (γ q p , 0, B) is the decision associated with q; -Else if for all k ≤ m q , δ(q, β q k ) ∈ Q ′ and there exists γ q p such that δ(q, γ q p ) ∈ Q ′ then q ∈ Q i+1 and defining B = {α q k | k ≤ k q ∧ δ(q, α q k ) / ∈ Q ′ }, (γ q p , 0, B) is the decision associated with q. By construction, for all q ∈ Q, one has q ∈ Q i if and only if delay * (q) = i. Furthermore delay s C (q) = delay * (q). Assume there exists a winning strategy s ′ C such that s C ≺ s ′ C . Since s C achieves the minimality of delay for states visited by s C , there must exist a state q visited by s C that belongs to some Q i such that s ′ C (q) is strictly more permissive than s C (q). By definition of s C (q), this implies that there exists a state q ′′ / ∈ j<i Q j which is the destination of a transition of Next(q, d). Thus delay s ′ C (q) > delay s C (q), establishing a contradiction. In order to obtain a linear time algorithm, one proceeds as follows. In the sequel i denotes the current iteration when the sets Q 0 , Q 1 , . . . , Q i-1 have been built. Here Q ′ denotes Q ′ = j≤i Q j .

-Initially one builds a "reverse graph" whose vertices are the states and there is an edge q ′ β q k -→ q (resp. q ′ γ q p -→ q) with k ≤ m q (resp. p ≤ p q ) if δ(q, β q k ) = q ′ (resp. δ(q, γ q p ) = q ′ ). -At beginning of the i th iteration, the set Q i has already been computed using the variables described below. -One associates a counter c q and a boolean b q with every state q and a boolean b q with every idle state q. Boolean b q is true if there exists some action γ q p such that δ(q, γ q p ) ∈ Q ′ and c q is the size of the set {k ≤ m q , δ(q, β q k ) / ∈ Q ′ }.

A state q belongs to Q if (1) it does not belong to Q ′ , (2) its counter c q is null, and (3) either it is transient or its boolean b q is true. -The i th iteration consists in two stages for all q ∈ Q i . First one determines s C (q) using the rules described above. Then one updates the counters and the booleans using the edges of the reverse graph: for all q β q ′ k --→ q ′ , c q ′ is decremented and if there exists some q γ q ′ p --→ q ′ b q ′ is set to true. If q ′ satisfies the three conditions w.r.t. iteration i + 1, it enters the set Q i+1 .

It is routine to check that this procedures operates in linear time.

⊓ ⊔

Conclusion

We have introduced a model of qualitative time concurrent game between a controller and an environment. We have designed a linear-time translation from such a game to an untimed turn-based game and shown that given any parity goal, the concurrent game is winning for the controller if and only if the turn-based game is winning for it. This allows us, taking as input a positional winning strategy of the turn-based game, to build in linear time a positional winning strategy in the original game. Furthermore we have introduced a notion of permissivity for strategies and we have established that one can compute in linear time a maximally permissive winning strategy for safety and reachability goals. For future work, we want to design an algorithm for computing in polynomial time a maximally permissive winning strategy for repeated reachability goals. We also plan to modify the notion of delay for reachability goals by integrating the delay of actions when computing a maximally permissive winning strategy for reachability. Finally our notion of qualitative delay for actions could be refined in order to take into account more precise (but still qualitative) information.

Fig. 2 :

 2 Fig. 2: Game structure of the case study


Caroline Collange
email: caroline.collange@inria.fr

Simty: generalized SIMT execution on RISC-V

Keywords: SIMT, SIMD, FPGA, RISC-V

come

INTRODUCTION

The Single Instruction, Multiple Threads (SIMT) execution model as implemented in NVIDIA Graphics Processing Units (GPUs) associates a multi-thread programming model with an SIMD execution model [START_REF] Nickolls | The GPU Computing Era[END_REF]. The flexibility obtained by running multi-thread programs on SIMD units makes SIMT attractive for heterogeneous many-core processors, where different cores may use different physical SIMD widths and multi-threading depths. However, current SIMT architectures demand specific instruction sets. In particular, they need specific branch instructions to manage thread divergence and convergence. SIMT GPUs have remained so far incompatible with traditional general-purpose CPU instruction sets.

We argue that the SIMT execution model can be generalized to a general-purpose instruction set at a very low hardware cost. As experimental evidence, we introduce Simty, a generalized-SIMT core that runs the RISC-V instruction set. Simty lifts the binary incompatibility between latency-oriented CPU cores and throughputoriented GPU-like cores by letting them share a single, unified instruction set. It enables commodity compilers, operating systems and programming languages to target GPU-like SIMT cores. Beside simplifying software layers, the unification of CPU and GPU instruction sets eases prototyping and debugging of parallel programs. We have implemented Simty in synthesizable VHDL and synthesized it for an FPGA target.

We present our approach to generalizing the SIMT model in Section 2, then describe Simty's microarchitecture is Section 3, and study an FPGA synthesis case Section 4.

CONTEXT

We introduce some background about the generalized SIMT model and clarify the terminology used in this paper.

General-purpose SIMT

The SIMT execution model consists in assembling vector instructions across different scalar threads of SPMD programs at the microarchitectural level. Current SIMT instruction sets are essentially scalar, with the exception of branch instructions that control thread divergence and convergence [START_REF] Collange | Stack-less SIMT reconvergence at low cost[END_REF]. Equivalently, an SIMT instruction set can be considered as a pure SIMD or vector instruction set with fully masked instructions, including gather and scatter instructions, and providing hardware-assisted management of a per-lane activity mask [START_REF] John | Computer architecture: a quantitative approach[END_REF]. The thread divergence and convergence hardware is exposed at the architecture level, so current SIMT instruction sets offer a variety of custom control-flow instruction instead of the usual conditional and indirect branches.

We have shown in prior work that the SIMT execution model could be generalized to general-purpose instruction sets, with no specific branch instructions [START_REF] Brunie | Simultaneous Branch and Warp Interweaving for Sustained GPU Performance[END_REF][START_REF] Collange | Stack-less SIMT reconvergence at low cost[END_REF]. This technique is amenable to an efficient representation of program counters using a sorted list [START_REF] Brunie | Simultaneous Branch and Warp Interweaving for Sustained GPU Performance[END_REF][START_REF] Collange | Path list traversal: a new class of SIMT flow tracking mechanisms[END_REF]. Simty implements a sorted path list with one active path.

Terminology

A multi-thread or multi-core processor exposes a fixed number of hardware threads, upon which the operating system schedules software threads. Unless specified otherwise, a thread will designate in the rest of the paper a hardware thread, or hart in RISC-V terminology. In an SIMT architecture, threads are grouped in fixed-size warps. This partitionning is essentially invisible to software.

Register file and execution units are organized in an SIMD fashion. The SIMD width corresponds to the number of threads in a warp. Each thread of a warp is statically assigned a distinct SIMD lane. Its context resides fully in a private register file associated with its lane. By virtue of the multi-thread programming model, there is no need for direct communication between registers of different lanes.

As the programming model is multi-thread, each thread has its own architectural Program Counter (PC). However, the microarchitecture does not necessarily implement these architectural PCs as separate physical registers. To account for thread-dependent control flow, we introduce an intermediate level between thread and warp that we call Path [START_REF] Collange | Path list traversal: a new class of SIMT flow tracking mechanisms[END_REF]. Each path tracks one of the different paths followed by threads in the program. The path concept is also found under the names warp-split [START_REF] Meng | Dynamic warp subdivision for integrated branch and memory divergence tolerance[END_REF], context [START_REF] Brunie | Simultaneous Branch and Warp Interweaving for Sustained GPU Performance[END_REF], fragment [START_REF] Lee | Exploring the Tradeoffs between Programmability and Efficiency in Data-Parallel Accelerators[END_REF], or instruction stream [START_REF] Kalathingal | Dynamic Inter-Thread Vectorization Architecture: extracting DLP from TLP[END_REF] in the literature. Threads of a path advance in lockstep and share a Common Program Counter (CPC) in the same address space. All threads in a given path belong to the same warp. Thus, each warp contains from 1 to 𝑚 paths, where 𝑚 is the number of threads per warp. The set of threads in a path is represented in hardware by an 𝑚-bit mask for each path. Mask bit 𝑖 of path 𝑗 is set when thread 𝑖 of the warp belongs to path 𝑗. We can represent the state of a warp equivalently either as a vector of 𝑚 PCs, or as a set of paths identified by (CPC, mask) pairs. In addition to the PC, the state of a path may contain information to help path scheduling, such as function call depth and privilege level.

Following branches in SIMT may be seen as traversing the control-flow graph. The processor follows one path of each warp, that we name the active path. The other paths are saved in a list. As threads of a warp take different directions through branches or get back to executing the same instructions, paths may diverge or converge.

• Control-flow divergence occurs when the active path encounters a branch, and its threads take different directions through the branch. It is implemented by splitting the active path into two new paths. One path is saved in the list, and execution continues on the other path. • Control-flow convergence is detected dynamically. It consists in merging the active path with a path of the list, or two paths of the list, when they have the same PC.

SIMTY MICROARCHITECTURE

We present design principles, then an overview of the Simty pipeline, and detail path tracking mechanisms.

Design principles

As an SIMD-based architecture, the key idea of Simty is to factor out control logic (instruction fetch, decode and scheduling logic) while replicating datapaths (registers and execution units). The pipeline is thus build around a scalar multi-thread front-end and an SIMD backend. General-purpose scalar ISA. We chose the RISC-V open instruction set, without any custom extension [START_REF] Waterman | The RISC-V Instruction Set Manual[END_REF]. Indeed, RISC-V is well-suited to many-thread architectures thanks to its small perthread state. Simty currently supports the RV32I subset (generalpurpose user-level instructions and 32-bit integer arithmetic) and a subset of privileged instructions for hardware thread management.

Throughput-oriented architecture. Simty focuses on exploiting thread-level parallelism across warps to hide execution latency, as well as data-level parallelism inside paths to increase throughput. On the other hand, the initial implementation of Simty does not attempt to leverage instruction-level parallelism beyond simple pipelined execution to focus on SIMT-specific aspects. For instance, in order to simplify bypass logic, a given warp cannot have instructions in two successive pipeline stages. This restriction matches the limitations of industrial designs like Nvidia Fermi GPUs [START_REF] Nickolls | The GPU Computing Era[END_REF] or Intel Xeon Phi Knights Corner [START_REF] Chrysos | Intel® Xeon Phi™ Coprocessor-the Architecture[END_REF].

Configurable. Warp and thread counts are configurable at RTL synthesis time. The typical design space we consider ranges between 4 warps × 4 threads and 16 warps × 32 threads, to target design points comparable to a Xeon Phi core [START_REF] Chrysos | Intel® Xeon Phi™ Coprocessor-the Architecture[END_REF] or an Nvidia GPU SM [START_REF] Nickolls | The GPU Computing Era[END_REF]. The RTL code is written in synthesizable VHDL. Pipeline stages are split into distinct components whenever possible to enable easy pipeline re-balancing or deepening. All internal memory including the register file is made of single read port, single write port SRAM blocks. This enables easy synthesis using FPGA block RAMs or generic ASIC macros.

Leader-follower resource arbitration. Simty uses an nonblocking pipeline to maximize multi-thread throughput and simplify control logic. Instruction scheduling obeys data dependencies. Execution hazards like resource conflicts are handled by partially replaying the conflicting instruction as follows.

When a path accesses a shared resource (e.g. a data cache bank), the arbitration logic gives access to an arbitrary leader thread of the path. All other threads of the path then check whether they can share the resource access with the leader (e.g. same cache block). Threads that do are considered as followers and also participate in the access. When at least one thread of the path is neither leader nor follower, the path is split in two paths. A path containing the leader and followers advances to the next instruction. Another path containing the other threads keeps the same PC to have the instruction eventually replayed. This partial replay mechanism guarantees global forward progress, as each access serves at least the leader thread.

PC-based commit. Program counters are used to track the progress of threads in paths. By relying on per-thread architectural PCs, the partial instruction replay mechanism is interruptible and has no atomicity requirement. Indeed, the architectural state of each thread stays consistent at all times, as the programming model does not enforce any order between instructions of different threads. This avoids the challenges of implementing precise exceptions in traditional vector processing [START_REF] Kozyrakis | Overcoming the limitations of conventional vector processors[END_REF].

The Simty pipeline

Simty is build around a 10-stage, single-issue, in-order pipeline as shown on Figure 1. We briefly describe each stage.

Fetch steering selects one warp and looks up the speculative CPC of its active path in a table indexed by the warp identifier. Warp scheduling currently follows a round-robin order. The speculative CPC is then updated to the predicted address of the next instruction. Currently, the prediction logic merely increments the CPC, though any actual branch predictor may be used instead.

Instruction Fetch/Predecode fetches an instruction word from the instruction cache or dedicated memory. A first predecode stage checks which operands reference registers. The RISC-V encoding enables a straightforward predecode logic to collect all the data that scoreboarding logic needs to track register dependencies between instructions. The predecoded instruction is placed in an instruction buffer containing one entry per warp.

Scheduler issues instructions when their operands are ready. A qualification step selects warps whose next instruction is ready to be executed. It considers both instruction dependencies and execution resource availability: bank conflicts in the register file are proactively avoided at this stage. A selection step then picks one of the ready warps marked by the qualification step. The current scheduling policy is loose round-robin: the first ready warp starting from the round-robin warp is selected. Other policies like pseudorandom scheduling are possible to avoid systematic conflicts in memory accesses.

Register File. Operand collection logic reads instruction operands from the register file (RF) during two pipeline stages. Each SIMD lane has its own RF. Each of these RFs is further partitioned into two banks based on the warp identifier. One bank handles warps of even ID, and the other bank handles warps of odd ID, an organization referred to as "thin" allocation [START_REF] Liu | Operand collector architecture[END_REF]. Each bank has a single read port and a single write port.

• For instructions that take two source register operands, registers are read serially from the same bank over two cycles. To avoid conflicts, the next instruction has to belong to a warp whose registers are in the other RF bank. This constraint is enforced by the scheduler stage. • For instructions that take a single source register operand, both banks are available to the next instruction.

The write port of each bank is available for writebacks from the ALUs. Output values from the memory access unit are opportunistically written back on free ports from a FIFO queue. Instructions are fully decoded at this stage.

Execute. Execution units consist of one 32-bit ALU supporting the RV32I instruction set in each lane. All arithmetic instructions are currently executed in a single cycle, though the design can accomodate pipelined floating point units and integer multipliers in the future.

Membership, HCT1 and HCT2 run concurrently with the execute stage. The membership stage recovers the path thread membership mask of the warp that identifies which threads are active. For arithmetic instructions, the mask is the eventual nonspeculative commit mask. For memory access instructions, it is a speculative mask under the assumption no exception occurs. From the mask, a priority encoder computes the identifier of the leader thread by finding the first bit set in the membership mask. The membership unit also detects convergence between paths. It is based on three tables HCT1, HCT2 and CCT in three successive pipeline stages, and will be described in more details in Section 3.3.

Writeback conditionally writes results from the array of execution units back to the respective RFs. For each lane 𝑖, the output is written back when bit 𝑖 of the membership mask is set. The mask can be all zeroes in case of branch misprediction. A bypass network also forwards the output to the input stage of execution units. The membership mask also controls the bypass network on a per-lane basis, in order to prevent an instruction that precedes a convergence point to forward stale data to instructions that follow the convergence point.

Branch. The branch unit splits paths when executing a divergent branch instruction. It takes as inputs a condition vector 𝑐 from the ALUs and the membership mask 𝑚 from the membership unit. Both conditional branches and indirect branches may diverge.

• For a conditional branch, the scalar destination address PC 𝑑 is computed from the PC and the instruction immediate. Two paths are created. One path tracks threads that follow the branch (PC 𝑑 , 𝑐 ∧ 𝑚), and a second path tracks threads that fall through the next instruction (PC + 4, c ∧𝑚). Empty paths are subsequently discarded. • An indirect branch which computed address vector contains multiple different targets may diverge into more than two paths. This case is handled as a resource conflict. Branches to each unique target are serialized in order to have at most two paths out of the branch unit at each time. Following the leader-follower strategy, all threads that have the same target PC 𝑙 as the leader take the branch, while the other threads keep the same PC and have the indirect branch instruction replayed.

Memory coalescing and Memory access. The memory arbiter coordinates the accesses that threads of a path perform concurrently to a shared memory or cache. It is optimized for two common cases: (1) when threads of a warp access consecutive words from the same cache block, and (2) when all threads access the same word. Both cases can be detected by comparisons between the address requested by each thread and the address requested by the leader thread. Threads that do not obey either pattern form a new path and their instruction is replayed.

Memory gather distributes data obtained from the cache block in memory back to the threads of the path. In particular, it can broadcast the word accessed by the leader thread to the other threads, as well as perform parallel access to aligned data in the cache line, akin to the coalescing rules of first-generation NVIDIA Tesla GPUs [START_REF] Lindholm | NVIDIA Tesla: A Unified Graphics and Computing Architecture[END_REF]. Future research will have to evaluate the design space and tradeoffs between such minimalist interconnect and a full crossbar.

Path tracking

The path tracking unit is responsible for three functions: (1) check thread membership within a path to compute the validity mask of an instruction, (2) merge the paths that have identical PC to let threads converge, and (3) select the active path that is followed by the front-end.

Simty leverages the path representation based on (CPC, mask) pairs presented in Section 2.2. Function 1 simply amounts to checking that the instruction address to commit is equal to the PC of the active path and reading the associated mask. Functions 2 and 3 are implemented based on a list of paths sorted by priority. The path with the highest priority is the active path. Priority is given to the path in the deepest nested function call level, and in case of a tie to the path with the minimal PC [START_REF] Collange | Stack-less SIMT reconvergence at low cost[END_REF]. As priorities are based on CPC values and there is a singe active path, path convergence only needs to be detected between the active path and the second path by priority order.

Path entries are kept sorted by function call level and PC. To manage efficiently a large number of paths in hardware, we isolate the two head paths, sorted on-line, from all other inactive paths, sorted off-line by a state machine. The head paths are kept in the Hot Context Tables (HCTs) indexed by the warp identifier which are accessed every cycle. The Cold Context Table (CCT) maintains the other, infrequently-accessed paths (Figure 2) [START_REF] Brunie | Simultaneous Branch and Warp Interweaving for Sustained GPU Performance[END_REF].

The sort/compact unit in Figure 2 gathers paths from the previous state of the warp, from the next PC and from the outputs of the branch unit and instruction replay logic. For any instruction, this represents at most 3 path. It then merges entries that have the same PC and same function call level, discards paths with empty masks and sorts the resulting paths by priority order. After compaction and sorting, the first two entries by priority order are stored in their respective HCT. When only a single valid path remains after compaction, it is stored in the HCT 1, while the new HCT 2 entry is popped from the head entry of the CCT. When three valid path remain, the third one is pushed to the head of the CCT.

The CCT size is adjusted for the worst case of one path per thread. It contains a stack of paths for each warp, which head is followed by a pointer. The offline sorting unit is a state machine with 3 states and one pointer per warp. It performs an iterative insertion sort opportunistically when the CCT ports are available. Each pointer walks through CCT entries of the warp, and the pointed entry is compared with the second HCT entry. When the order does not match the desired priority order, these entries are swapped atomically. Together with the online compaction-sorting network, the offline sorting state machine eventually converges toward a fully sorted path list in at most 𝑚 2 steps with 𝑚-thread warps. The performance of this low-overhead implementation is adequate for the purpose of sorting paths, as CCT sorting only occurs in the case of unstructured control flow, and the order of paths does not affect correctness.

FPGA IMPLEMENTATION

We illustrate and evaluate an implementation of Simty on an FPGA target. Circuit synthesis for FPGAs is a first prototyping step toward hardware synthesis. It also represents an application in its own right: Simty can serve as a parallel controller for a reconfigurable accelerator, as an alternative to vector soft-core processors [START_REF] Severance | Soft vector processors with streaming pipelines[END_REF]. We synthesized and tested Simty on an Altera Cyclone IV EP4CE115 FPGA of an Altera DE-2 115 development board, for a target frequency of 50 MHz.

The main microarchitectural parameters are the warp count 𝑛 and the warp width 𝑚. Warp width determines the number of parallel execution units and thus the execution throughput of a core. A Simty architecture with few cores and wide warps will benefit applications which threads present an homogeneous behavior and that take advantage from dynamic vectorization. Conversely, more cores with narrower warps will offer a more stable performance on irregular parallel code. Warp count determines tolerance to execution latency, especially from external memory.

Figure 3 presents synthesis results after place-and-route as a function of thread and warp count. The architecture scales up to 64 warps × 32 threads and 8 warps × 64 threads. The cost of control logic is amortized over SIMD execution units. The sweet spot on this platform is obtained between 8 warps × 8 threads and 32 warps × 16 threads. Beyond this point, routing congestion causes a sensible cycle time increase and the extra area gains against multiple Simty cores are low.

These results show that the overhead of generalized SIMT can be easily amortized, even in the context of a microcontroller-class single-issue RISC pipeline. As we add execution resources such as integer multipliers and floating-point units, we expect the cost of the path tracking logic will eventually become negligible.

RELATED WORK

Simty complements the existing set of open-source tools of the parallel architecture and GPU research communities. Multiple opensource cycle-level simulators of GPU architectures are available, including GPGPU-Sim [START_REF] Bakhoda | Analyzing CUDA Workloads Using a Detailed GPU Simulator[END_REF], MV5 [START_REF] Meng | A reconfigurable simulator for largescale heterogeneous multicore architectures[END_REF], Barra [START_REF] Sylvain Collange | Barra: a Parallel Functional Simulator for GPGPU[END_REF], SST-MacSim [START_REF] Kim | Macsim: A CPU-GPU heterogeneous simulation framework user guide[END_REF] and Multi2Sim [START_REF] Gong | Multi2Sim Kepler: A detailed architectural GPU simulator[END_REF]. Software-based simulators can be used to evaluate timing and sometimes energy consumption, but give no direct indication of hardware implementation cost. Simulation also incurs a slowdown of multiple orders of magnitude compared to actual hardware.

To address these limitations of simulators, several hardwaresynthesizable parallel processors have been recently released in the academic community. They include vector processors, SIMD cores, and GPU-based architectures.

Vector processors. HWACHA is a synthesizable vector processors running vector instruction set extensions to RISC-V [START_REF] Lee | A 45nm 1.3 GHz 16.7 doubleprecision GFLOPS/W RISC-V processor with vector accelerators[END_REF]. Vector soft-cores such as VectorBlox MXP target FPGAs [START_REF] Severance | Soft vector processors with streaming pipelines[END_REF]. Vector processors traditionally rely on explicit vector instruction sets. For instance, HWACHA augments RISC-V with one set of vector instructions as well as two sets of scalar instructions.

SIMD cores. Guppy is a processor based on Leon that runs a SPARC-based SIMD instruction set with basic predication support [START_REF] Al-Dujaili | Guppy: A GPU-like soft-core processor[END_REF]. Nyuzi is a multi-thread SIMD processor for graphics rendering [START_REF] Bush | Nyami: a synthesizable GPU architectural model for general-purpose and graphics-specific workloads[END_REF]. GPU-based architectures. Kingyens and Steffan propose a processor compatible with the fragment shader unit of the ATI R500 GPU architecture [START_REF] Kingyens | A GPU-inspired soft processor for high-throughput acceleration[END_REF]. MIAOW is a synthesizable GPU based on the AMD GCN architecture [START_REF] Balasubramanian | Enabling GPGPU low-level hardware explorations with MIAOW: an open-source RTL implementation of a GPGPU[END_REF]. Flexgrip [START_REF] Andryc | FlexGrip: A soft GPGPU for FPGAs[END_REF] is a GPU based on the Nvidia Tesla architecture that follows the pipeline of the Barra simulator [START_REF] Sylvain Collange | Barra: a Parallel Functional Simulator for GPGPU[END_REF].

All the aforementioned processors are based either on explicit vector or SIMD instruction sets with per-lane predication, either on SIMT instruction sets with custom control flow instructions. Like Simty, the Maven architecture [START_REF] Lee | Exploring the Tradeoffs between Programmability and Efficiency in Data-Parallel Accelerators[END_REF] uses a unified instruction set for both its scalar control thread and its vector micro-threads, but its RTL implementation is not publicly available. To our knowledge, Simty is the first open-source RTL-level SIMT processor that supports a scalar general-purpose instruction set.

FUTURE WORK

As a proof of concept, the initial Simty implementation focuses on clarity and simplicity. Following this proof of concept, we intend to incorporate floating-point, atomic and privileged instructions, and virtual memory support, as well as bringing up the software infrastructure, relying on RISC-V support in existing compiler toolchains and operating systems.

As in all conventional SIMT architectures prior to Nvidia Volta, thread synchronization and scheduling policies in Simty only guarantee global progress, ensuring at least one thread makes forward progress. However, individual threads have no guarantee of forward progress. Busy waiting loops may thus cause deadlocks [START_REF] Eltantawy | MIMD Synchronization on SIMT Architectures[END_REF]. Thus, the current implementation requires all inter-thread synchronization to use explicit instructions. In order to run more general SPMD code, path scheduling policies that balance fairness with convergence timeliness will be needed [START_REF] Kalathingal | Dynamic Inter-Thread Vectorization Architecture: extracting DLP from TLP[END_REF].

CONCLUSION

Simty demonstrates the hardware feasibility of microarchitecturelevel SIMT. It implements the SIMT execution model purely at the microarchitecture level, preserving a scalar general-purpose instruction set at the architecture level. As such, it provides a building block for massively parallel many-core processors. Together with the rest of the RISC-V ecosystem, Simty provides an open platform for research on GPU micro-architecture, on hybrid CPU-GPU micro-architecture, or on heterogeneous platforms with throughput-optimized cores.

SOURCE CODE

Simty is distributed under a GPL-compatible CeCILL license at https://gitlab.inria.fr/collange/simty.

Figure 1 :

 1 Figure 1: Simty pipeline.

Figure 2 :

 2 Figure 2: Detail of path tracking using path tables

Figure 3 :

 3 Figure3: Simty scaling on Altera Cyclone IV as a function of threads per warp 𝑚 and warp count 𝑛. Frequency is the worst-case estimate at 85°C in MHz. Area is given in Logic Elements (LEs) and in 128 × 32-bit RAM block (M9K) count. Place-and-route fails on configurations with {16, 32, 64} warps × 64 threads as a result of routing congestion.