Wen Kokke
email: wen.kokke@ed.ac.uk

J Garrett Morris

Philip Wadler
email: wadler@inf.ed.ac.uk

J Garrett Morris

Towards Races in Linear Logic

Keywords: π-calculus, linear logic, session types, non-determinism, deadlock freedom

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Consider the following scenario: Ami and Boé are working from home one morning when they each get a craving for a slice of cake. Being denizens of the web, they quickly find the nearest store which does home deliveries. Unfortunately for them, they both order their cake at the same store, which has only one slice left. After that, all it can deliver is disappointment. This is an example of a race condition. We can model this scenario in the πcalculus, where , and are processes modelling Ami, Boé and the store, and and are channels giving access to a slice of cake and disappointment, respectively. This process has two possible outcomes: either Ami gets the cake, and Boé gets disappointment, or vice versa. While Ami or Boé may not like all of the outcomes, it is the store which is responsible for implementing the online delivery service, and the store is happy with either outcome. Thus, the above is an interaction we would like to be able to model. Now consider another scenario, which takes place after Ami has already bought the cake:

Boé is really disappointed when she finds out the cake has sold out. Ami, always looking to make some money, offers to sell the slice to her for a profit. Boé agrees to engage in a little bit of back-alley cake resale, but sadly there is no trust between the two. Ami demands payment first. Boé would rather get her slice of cake before she gives Ami the money. This is an example of a deadlock. We can also model this scenario in the πcalculus, where is a channel giving access to some adequate amount of money.

(x(z).y[ ]. | y(w).x[ ]. ) =⇒

The above process does not reduce. As both Ami and Boé would prefer the exchange to be made, this interaction is desired by neither. Thus, the above is an interaction we would like to exclude.

Session types [START_REF] Honda | Types for dyadic interaction[END_REF] statically guarantee that concurrent programs, such as those above, respect communication protocols. Session-typed calculi with logical foundations, such as πDILL [START_REF] Caires | Session Types as Intuitionistic Linear Propositions[END_REF] and CP [START_REF] Wadler | Propositions as sessions[END_REF], obtain deadlock freedom as a result of a close correspondence with logic. These systems, however, also rule out non-determinism and race conditions. In this paper, we demonstrate that logicinspired type systems need not rule out races.

We present HCP - ND , an extension of CP with a novel account of non-determinism and races. Inspired by bounded linear logic [START_REF] Girard | Bounded linear logic: A modular approach to polynomial-time computability[END_REF], we introduce a form of shared channels in which the type of a shared channel tracks how many times it is reused. As in the untyped π-calculus, sharing introduces the potential for nondeterminism. We show that our approach is sufficient to capture practical examples of races, such as an online store, as well as other formal characterizations of non-determinism, such as non-deterministic choice. However, HCP - ND does not lose the meta-theoretical benefits of CP: we show that it enjoys termination and deadlock-freedom.

An important limitation of our work is that types in HCP - ND explicitly count the potential races on a channel. It works fine when there are two or three races, but not n for an arbitary n. The latter case is obviously important, and we see the main value of our work as a stepping stone to this more general case.

HCP - ND is based on HCP [START_REF] Kokke | Taking linear logic apart[END_REF][START_REF] Kokke | Better late than never: A fully-abstract semantics for classical processes[END_REF]. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP.

There are two versions of HCP: a version with delayed actions, introduced by Kokke, Montesi, and Peressotti [START_REF] Kokke | Better late than never: A fully-abstract semantics for classical processes[END_REF]; and a version without delayed actions, introduced by Kokke, Montesi, and Peressotti [START_REF] Kokke | Taking linear logic apart[END_REF], referred to as HCP -. In this work, we will base ourselves on the latter, as the former does not yet have reduction semantics.

This paper proceeds as follows. In section 2, we discuss recent approaches to non-determinism in logic-inspired session-typed process calculi. In section 3, we introduce a variant of CP and prove progress and preservation. In section 4, we introduce HCP - ND . In section 5, we discuss cuts with leftovers. Finally, in section 7, we conclude with a discussion of the work done in this paper and potential avenues for future work.

P Γ Q Γ P + Q Γ P + Q =⇒ P P + Q =⇒ Q
Local choice introduces non-determinism explicitly, by listing all possible choices. This is unlike the π-calculus, where non-determinism arises due to multiple processes communicating on shared channels. We can easily implement local choice in the π-calculus, using a nullary communication:

(x[].0 | x().P | x().Q) =⇒ (P | x().Q) or (x().P | Q)
In this implementation, the process x[].0 will "unlock" either P or Q, leaving the other process deadlocked. Or we could use input-guarded choice:

(x[].0 | (x().P + x().Q))
However, there are many non-deterministic processes in the π-calculus that are awkward to encode using non-deterministic local choice. Let us recall our example:

(x[ ].x[ ]. | x(y). | x(z). ) =⇒ ( | { /y} | { /z}) or ( | { /y} | { /z})
This non-deterministic interaction involves communication. If we wanted to write down a process which exhibited the same behaviour using non-deterministic local choice, we would have to write the following process:

(x[ ].y[ ]. | x(z). | y(w). ) + (y[ ].x[ ]. | x(z). | y(w). ) =⇒ ( | { /y} | { /z}) or ( | { /y} | { /z})
In essence, instead of modelling a non-deterministic interaction, we are enumerating the resulting deterministic interactions. This means non-deterministic local choice cannot model non-determinism in the way the π-calculus does. Enumerating all possible outcomes becomes worse the more processes are involved in an interaction. Imagine the following scenario:

Three customers, Ami, Boé, and Cat, have a craving for cake. Should cake be sold out, however, well... a doughnut will do. They prepare to order their goods via an online store. Unfortunately, they all decide to use the same shockingly under-stocked store, which has only one slice of cake, and a single doughnut. After that, all it can deliver is disappointment.

We can model this scenario in the π-calculus, where , , , and are four processes modelling Ami, Boé, Cat, and the store, and , , and are three channels giving access to a slice of cake, a so-so doughnut, and disappointment, respectively.

( | { /y} | { /z} | { /w}) or ( | { /y} | { /z} | { /w})
With the addition of one process, modelling Cat, we have increased the number of possible outcomes enormously! In general, the number of outcomes for these types of scenarios is n!, where n is the number of processes. This means that if we wish to translate any non-deterministic process to one using non-deterministic local choice, we can expect a factorial growth in the size of the term.

Hypersequent Classical Processes

In this section, we introduce HCP [START_REF] Kokke | Taking linear logic apart[END_REF][START_REF] Kokke | Better late than never: A fully-abstract semantics for classical processes[END_REF], the basis for our calculus HCP - ND . The term language for HCP -is a variant of the π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF].

P | Q ≡ Q | P (|-assoc) P | (Q | R) ≡ (P | Q) | R (halt) P | 0 ≡ P (scope-ext) (νx)(P | Q) ≡ P | (νx)Q if x ∈ P
Channels in HCP -are typed using a session type system which is a conservative extension of linear logic.

Definition 3 (Types).

A, B, C ::

= A ⊗ B independent channels | 1 unit for ⊗ | A B interdependent channels | ⊥ unit for | A ⊕ B internal choice | 0 unit for ⊕ | A B external choice | unit for
Duality plays a crucial role in both linear logic and session types. In HCP -, the two endpoints of a channel are assigned dual types. This ensures that, for instance, whenever a process sends across a channel, the process on the other end of that channel is waiting to receive. Each type A has a dual, written A ⊥ . Duality (• ⊥ ) is an involutive function on types.

Definition 4 (Duality)

.

(A ⊗ B) ⊥ = A ⊥ B ⊥ 1 ⊥ = ⊥ (A B) ⊥ = A ⊥ ⊗ B ⊥ ⊥ ⊥ = 1 (A ⊕ B) ⊥ = A ⊥ B ⊥ 0 ⊥ = (A B) ⊥ = A ⊥ ⊕ B ⊥ ⊥ = 0
Environments associate channels with types. Names in environments must be unique, and environments Γ and ∆ can only be combined (Γ , ∆) if cn(Γ ) ∩ cn(∆) = ∅, where cn(Γ ) denotes the set of channel names in Γ .

Definition 5 (Environments). Γ , ∆, Θ ::= x 1 : A 1 . . . x n : A n HCP -registers parallelism using hyper-environments. A hyper-environment is a multiset of environments. While names within environments must be unique, names may be shared between multiple environments in a hyper-environment.

We write G | H to combine two hyper-environments.

Definition 6 (Hyper-environments). G, H

::= ∅ | G | Γ
Typing judgements associate processes with collections of typed channels.

Definition 7 (Typing judgements). A typing judgement P Γ 1 | . . . | Γ n denotes that the process P consists of n independent, but potentially entangled processes, each of which communicates according to its own protocol Γ i . Typing judgements can be constructed using the inference rules below.

Structural rules

Ax x↔y

x : A, y :

A ⊥ P G | Γ, x : A | ∆, x : A ⊥ Cut (νx)P G | Γ , ∆ P G Q H H-Mix P | Q G | H H-Mix 0 0 ∅ Logical rules P G | Γ , y : A | ∆, x : B ⊗ x[y].P G | Γ , ∆, x : A ⊗ B P G | Γ, y : A, x : B ( ) x(y).P G | Γ, x : A B P G 1 x[].P G | x : 1 P G | Γ (⊥) x().P G | Γ, x : ⊥ P G | Γ, x : A (⊕ 1 ) x inl.P G | Γ, x : A ⊕ B P G | Γ, x : B (⊕ 2 ) x inr.P G | Γ, x : A ⊕ B P Γ, x : A Q Γ, x : B ( ) x {inl : P ; inr : Q} Γ, x : A B (no rule for 0) ( ) x {} Γ, x :
Furthermore, each logical rule has the side condition that x ∈ G.

Reductions relate processes with their reduced forms.

Definition 8 (Reduction). Reductions are described by the smallest relation =⇒ on process terms closed under the rules below:

(↔) (νx)(w↔x | P ) =⇒ P {w/x} (β⊗ ) (νx)(x[y].P | x(y).R) =⇒ (νx)(νy)(P | R) (β1⊥) (νx)(x[].P | x().Q) =⇒ P | Q (β⊕ 1 ) (νx)(x inl.P | x {inl : Q; inr : R}) =⇒ (νx)(P | Q) (β⊕ 2 ) (νx)(x inr.P | x {inl : Q; inr : R}) =⇒ (νx)(P | R) P =⇒ P (γν) (νx)P =⇒ (νx)P P =⇒ P (γ|) P | Q =⇒ P | Q P ≡ Q Q =⇒ Q Q ≡ P (γ≡) P =⇒ P

Example

HCP -uses hyper-sequents to structure communication, and it is this structure which rules out deadlocked interactions. Let us go back to our example of a deadlocked interaction from section 1. If we want to type this interaction in HCP -, we run into a problem: to communicate on x, we need to add name restrictions on x and y, e.g.,

(νx)(νy)(x(z).y[ ]. | y(w).x[ ]. ).
However, there is no typing derivation for this term. We illustrate this with the partial typing derivation below. In this derivation, there is no way to proceed and type the final name restriction. The Cut rule needs a hypersequent separator to eliminate, so that it only ever links up two independent processes, but the bottom-most sequent has none. Furthermore, the two occurrences of x appearing in the same environment make it ill-formed.

Γ, z :

⊥ , :

⊗ y[ ].
Γ, z : ⊥ , y :

x(z).y[ ].

Γ, x : ⊥ , y :

∆, : , w :

⊥ ⊗ x[ ].
∆, x : , w :

⊥ y(w).x[ ]. ∆, x : , y : ⊥ H-Mix (x(z).y[ ]. | y(w).x[ ]. ) Γ, x : ⊥ , y : | ∆, x : , y : ⊥ Cut (νy)(x(z).y[ ]. | y(w).x[ ]. )
Γ, ∆, x : ⊥ , x :

Metatheory

HCP -enjoys subject reduction, termination, and progress [START_REF] Kokke | Taking linear logic apart[END_REF].

Lemma 9 (Preservation for ≡).

If P ≡ Q, then P G iff Q G.
Proof. By induction on the derivation of P ≡ Q.

Theorem 10 (Preservation).

If P G and P =⇒ Q, then Q G.
Proof. By induction on the derivation of P =⇒ Q.

Definition 11 (Actions).

A process P acts on x whenever x is free in the outermost term constructor of P , e.g., x[y].P acts on x but not on y, and x↔y acts on both x and y. A process P is an action if it acts on some channel x.

Definition 12 (Canonical forms). A process P is in canonical form if

P ≡ (νx 1 ) . . . (νx n )(P 1 | • • • | P n+m+1 ),
such that: no process P i is a cut or a mix; no process P i is a link acting on a bound channel x i ; and no two processes P i and P j are acting on the same bound channel x i .

Lemma 13. If a well-typed process P is in canonical form, then it is blocked on an external communication, i.e., P ≡ (νx 1 ) . . .

(νx n )(P 1 | • • • | P n+m+1
) such that at least one process P i acts on a free name.

Proof. We have P ≡ (νx 1 ) . . . (νx n )(P 1 | . . . | P n+m+1 ), such that no P i is a cut or a link acting on a bound channel, and no two processes P i and P j are acting on the same bound channel. The prefix of cuts and mixes introduces n channels. Each application of cut requires an application of mix, so the prefix introduces n + m + 1 processes. Therefore, at least m + 1 of the processes P i must be acting on a free channel, i.e., blocked on an external communication.

Theorem 14 (Progress). If P Γ , then either P is in canonical form, or there exists a process Q such that P =⇒ Q.

Proof. We consider the maximum prefix of cuts and mixes of P such that P ≡ (νx 1 ) . . . (νx n )(P 1 | . . . | P n+m+1 ), and no P i is a cut. If any process P i is a link, we reduce by (↔). If any two processes P i and P j are acting on the same channel x i , we rewrite by ≡ and reduce by the appropriate β-rule. Otherwise, P is in canonical form.

Theorem 15 (Termination). If P G, then there are no infinite =⇒reduction sequences.

Proof. Every reduction reduces a single cut to zero, one or two cuts. However, each of these cuts is smaller, measured in the size of the cut formula. Furthermore, each instance of the structural congruence preserves the size of the cut. Therefore, there cannot be an infinite =⇒-reduction sequence.

Shared Channels and Non-determinism

In this section, we will discuss our main contribution: an extension of HCP - which allows for races while still excluding deadlocks. We have seen in section 3.1 how HCP -excludes deadlocks, but how exactly does HCP -exclude races? Let us return to our example from section 1, to the interaction between Ami, Boé and the store.

(x[ ].x[ ]. | x(y). | x(z). ) =⇒ ( | { /y} | { /z}) or ( | { /y} | { /z})
Races occur when more than two processes attempt to communicate simultaneously over the same channel. However, the Cut rule of HCP -requires that exactly two processes communicate over each channel:

P G | Γ, x : A | ∆, x : A ⊥ Cut (νx)P G | Γ , ∆
We could attempt to write down a protocol for our example, stating that the store has a pair of channels x, y : with which it communicates with Ami and Boé, taking to be the type of interactions in which cake may be obtained, i.e. of both and , and state that the store communicates with Ami and Boé over a channel of type . However, this only models interactions such as the following:

Γ, x : ⊥ ∆, y : ⊥ H-Mix ( | ) Γ, x : ⊥ | ∆, x : ⊥ ⊗ y[x].( | ) Γ, ∆, y : ⊥ ⊗ ⊥ Θ, x : , y : y(x).
Θ, y :

H-Mix (y[x].( | ) | y(x). ) ∆, y : ⊥ ⊗ ⊥ | Θ, y : Cut (νy)(y[x].( | ) | y(x). ) Γ, ∆, Θ
In this interaction, Ami will get whatever the store decides to send on x, and Boé will get whatever the store decides to send on y. This means that this interactions gives the choice of who receives what to the store. This is not an accurate model of our original example, where the choice of who receives the cake is non-deterministic and depends on factors outside of any of the participants' control! Modelling racy behaviour, such as that in our example, is essential to describing the interactions that take place in realistic concurrent systems. We would like to extend HCP -to allow such races in a way which mirrors the way in which the π-calculus handles non-determinism. Let us return to our example:

(x[ ].x[ ]. | x(y). | x(z). )
In this interaction, we see that the channel x is only used as a way to connect the various clients, Ami and Boé, to the store. The real communication, sending the slice of cake and disappointment, takes places on the channels , , y and z. Inspired by this, we add two new constructs to the term language of HCP - for sending and receiving on a shared channel. These actions are marked with a to distinguish them from ordinary sending and receiving.

Definition 16 (Terms). We extend definition 1 as follows:

P , Q, R ::= . . .

| x[y].P client creation

| x(y).P server interaction

As before, round brackets denote input, square brackets denote output. Note that x[y].P , much like x[y].P , is a bound output: both client creation and server interaction bind a new name. The structural congruence, which identifies certain terms, is the same as definition 2.

In any non-deadlock interaction between a server and some clients, there must be exactly as many clients as there are server interactions. Therefore, we add two new dual types for client pools and servers, which track how many clients or server interactions they represent.

Definition 17 (Types). We extend definition 3 as follows:

A, B, C ::= . . . | ! n A pool of n clients | ? n A n server interactions
The types ! n A and ? n A ⊥ are dual. Duality remains an involutive function.

We have to add typing rules to associate our new client and server interactions with their types. The definition for environments will remain unchanged, but we will extend the definition for the typing judgement. To determine the new typing rules, we essentially answer the question "What typing constructs do we need to complete the following proof?" Γ, y : The constructs x[y].P and x(y).P introduce a single client or server action, respectively-hence, channels of type ! 1 and ? 1 . However, when we cut, we want to cut on both interactions simultaneously. We need rules for the contraction of shared channel names.

Clients and Pooling

A client pool represents a number of independent processes, each wanting to interact with the same server. Examples of such a pool include Ami and Boé from our example, customers for online stores in general, and any number of processes which interact with a single, centralised server. We introduce two new rules: one to construct clients, and one to pool them together. The first rule, (! 1 ), interacts over a channel as a client. It does this by receiving a channel y over a shared channel x. The channel y is the channel across which the actual interaction will eventually take place. The second rule, Cont ! , allows us to contract shared channel names with the same type. When used together with H-Mix, this allows us to pool clients together.

P G | Γ, y : A (! 1 ) x[y].P G | Γ, x : ! 1 A P G | Γ, x : ! m A | ∆, y : ! n A Cont ! P {x/y} G | Γ, ∆, x : ! m+n A
Using these rules, we can derive the left-hand side of our proof by marking Ami and Boé as clients, and pooling them together.

Γ, y :

⊥ (! 1 ) x[y]. Γ, y : ! 1 ⊥ ∆, y : ⊥ (! 1 ) x [y ]. ∆, x : ! 1 ⊥ H-Mix ( x[y]. | x [y ]. ) Γ, x : ! 1 ⊥ | ∆, x : ! 1 ⊥ Cont ! ( x[y]. | x[y ]. ) Γ, ∆, x : ! 2 ⊥

Servers and Sequencing

Dual to a pool of n clients in parallel is a server with n actions in sequence. Our interpretation of a server is a process which offers some number of interdependent interactions of the same type. Examples include the store from our example, which gives out slices of cake and disappointment, online stores in general, and any central server which interacts with some number of client processes.

We introduce two new rules to construct servers. The first rule, (? 1 ), marks a interaction over some channel as a server interaction. It does this by sending a channel y over a shared channel x. The channel y is the channel across which the actual interaction will take place. The second rule, Cont ? , allows us to merge two (possibly interleaved) sequences of server interactions. This allows us to construct a server which has multiple interactions of the same type, across the same shared channel. Using these rules, we can derive the right-hand side of our proof, by marking each of the store's interactions as server interactions, and then contracting them.

Θ, z : , z : (? 1 ) x (z ).

Θ, z : , x : ? 1 (? 1 ) x(z). x (z ).

Θ, x : ? 1 , x : ? 1 Cont ? x(z). x(z ).

Θ, x : ? 2 Thus, we complete the typing derivation of our example.

Definition 18 (Typing judgements). We extend definition 7 as follows:

P G | Γ, y : A (! 1 ) x[y].P G | Γ, x : ! 1 A P G | Γ, y : A (? 1 ) x(y).P G | Γ, x : ? 1 A P G | Γ, x : ! m A | ∆, y : ! n A Cont ! P {x/y} G | Γ, ∆, x : ! m+n A P G | Γ, x : ? m A, y : ? n A Cont ? P {x/y} G | Γ, x : ? m+n A

Running Clients and Servers

Finally, we need to extend the reduction rules to allow for the reduction of client and server processes. The reduction rule we add is a variant of the reduction rule for ⊗ and , (β⊗ ).

Definition 19 (Reduction). We extend definition 8 as follows:

(β ) (νx)(( x[y].P | x(z).Q) | R) =⇒ (νx)((νy)(P | Q{y/z}) | R)
The difference between (β ) and (β⊗ ) is that the former allows reduction to happen in the presence of an unrelated process R, which is passed along unchanged. This is necessary, as there may be other clients waiting to interact with the server on the shared channel x, which cannot be moved out of scope of the name restriction (νx). When there is no unrelated process R, i.e., when there is only a single client, we can rewrite by (halt) before and after applying (β ). So where does the non-determinism in HCP - ND come from? Let us say we have a term of the following form:

(νx)(( x[y 1 ].P 1 | • • • | x[y n ].P n ) | x(y 1 ). . . . x(y n ).Q)
As parallel composition is commutative and associative, we can rewrite this term to pair any client in the pool with the server before applying (β ). Thus, like in the π-calculus, the non-determinism is introduced by the structural congruence. Does this mean that, for an arbitrary client pool P in (νx)(P | x(z).Q), every client in that pool is competing for the server interaction on x? Not necessarily, as some portion of the clients can be blocked on an external communication. For instance, in the term below, clients n+1 ].P n+1 . . . x[y m ].P m are blocked on a communication on the external channel a:

νx.(( ( x[y 1 ].P 1 | • • • | x[y n ].P n ) | a().( x[y n+1 ].P n+1 | • • • | x[y m ].P m ) ) | x(y 1 ). . . . x(y m ).Q )
If we reduce this term, then only the clients x[y 1 ].P 1 . . . x[y n ].P n will be assigned server interactions, and we end up with the following canonical form:

νx.( a().( x[y n+1 ].P n+1 | • • • | x[y m ].P m ) | x(y n+1 ). . . . x(y m ).Q )
This matches our intuition and the behaviour of the π-calculus.

Alternative syntax. If we choose to reuse the terms x[y].P and x(y).P for shared channels, we could replace (β⊗ ) with (β ), using the latter rule for both cases.

Metatheory

HCP - ND enjoys subject reduction, termination, and progress. Lemma 20 (Preservation for ≡).

If P ≡ Q and P G, then Q G.
Proof. By induction on the derivation of P ≡ Q.

Theorem 21 (Preservation).

If P G and P =⇒ Q, then Q G.
Proof. By induction on the derivation of P =⇒ Q.

Definition 22 (Actions). A process P acts on x whenever x is free in the outermost term constructor of P , e.g., x(y).P acts on x but not on y, and x↔y acts on both x and y. A process P is an action if it acts on some channel x. Two actions are dual when they introduce dual type constructors, e.g., x[y].P is dual to x(z).Q, but x↔y is not dual to any action.

Definition 23 (Canonical forms). A process P is in canonical form if

P ≡ (νx 1 ) . . . (νx n )(P 1 | • • • | P n+m+1 ),
such that: no process P i is a cut or a mix; no process P i is a link acting on a bound channel x i ; and no two processes P i and P j are acting on the same bound channel x i with dual actions.

The new definition of canonical forms is slightly more precise than definition 12: we added the phrase "with dual actions". With the addition of shared channels, it has become possible to have a process which cannot reduce, but in which two processes are waiting to act on the same channel, e.g., in (

x[y]. | x[y ]. ).
Lemma 24. If a well-typed process P is in canonical form, then it is blocked on an external communication, i.e., P ≡ (νx 1 ) . . .

(νx n )(P 1 | • • • | P n+m+1
) such that at least one process P i acts on a free name.

Proof. We have P ≡ (νx 1 ) . . . (νx n )(P 1 | . . . | P n+m+1 ), such that no P i is a cut or a link acting on a bound channel, and no two processes P i and P j are acting on the same bound channel with dual actions. The prefix of cuts and mixes introduces n channels. Each application of cut requires an application of mix, so the prefix introduces n + m + 1 processes. Each application of Cont ! requires an application of mix, so there are at most m clients acting on the same bound channel. Therefore, at least one of the processes P i must be acting on a free channel, i.e., blocked on an external communication.

Theorem 25 (Progress). If P Γ , then either P is in canonical form, or there exists a process Q such that P =⇒ Q.

Proof. We consider the maximum prefix of cuts and mixes of P such that P ≡ (νx 1 ) . . . (νx n )(P 1 | . . . | P n+m+1 ), and no P i is a cut. If any process P i is a link, we reduce by (↔). If any two processes P i and P j are acting on the same channel x i with dual actions, we rewrite by ≡ and reduce by the appropriate β-rule. Otherwise, P is in canonical form.

Theorem 26 (Termination). If P G, then there are no infinite =⇒reduction sequences.

Proof. Every reduction reduces a single cut to zero, one or two cuts. However, each of these cuts is smaller, measured in the size of the cut formula. Furthermore, each instance of the structural congruence preserves the size of the cut. Therefore, there cannot be an infinite =⇒-reduction sequence.

HCP - ND and Non-deterministic Local Choice

In section 2, we discussed the non-deterministic local choice operator, which is used in several extensions of πDILL and CP [START_REF] Atkey | Conflation confers concurrency[END_REF][START_REF] Caires | Types and logic, concurrency and non-determinism[END_REF][START_REF] Caires | Linearity, control effects, and behavioral types[END_REF]. This operator is admissible in HCP - ND . We can derive the non-deterministic choice P + Q by constructing the following term: -On the right-hand side, we have a server with both P and Q. This server has two channels on which a choice is offered, y and z. The choice on y selects between P and Q. The choice on z does not affect the outcome of the process at all. Instead, it is discarded.

When these clients and the server are put together, the choices offered by the server will be non-deterministically lined up with the clients which make choices, and either P or Q will run. While there is a certain amount of overhead involved in this encoding, it scales linearly in terms of the number of processes. The reverse-encoding the non-determinism present in HCP - ND using non-deterministic local choice-scales exponentially, see, e.g., the examples in section 2.

Cuts with Leftovers

So far, our account of a non-determinism in client/server interactions only allows for interactions between equal numbers of clients and server interactions. A natural question is whether or not we can deal with the scenario in which there are more client than server interactions or vice versa, i.e., whether or not the following rules are derivable:

Γ, ! n+m A ∆, ? n A ⊥ Γ, ∆, ! m A Γ, ! n A ∆, ? n+m A ⊥ Γ, ∆, ? m A ⊥
These rules are derivable using a link. For instance, we can derive the rule for the case in which there are more clients than servers as follows:

P Γ, x : ! n+m A Q ∆, x : ? n A ⊥ x↔w x : ? m A ⊥ , w : ! m A H-Mix (Q | x↔w) ∆, x : ? n A ⊥ | x : ? m A ⊥ , w : ! m A Cont ! (Q | x↔w) ∆, x : ? n+m A ⊥ , w : ! m A H-Mix (P | (Q | x↔w)) Γ, x : ! n+m A | ∆, x : ? n+m A ⊥ , w : ! m A Cut (νx)(P | (Q | x↔w)) Γ, ∆, w : ! m A 6

Relation to Manifest Sharing

In section 2, we mentioned related work which extends πDILL and CP with nondeterministic local choice [START_REF] Atkey | Conflation confers concurrency[END_REF][START_REF] Caires | Types and logic, concurrency and non-determinism[END_REF][START_REF] Caires | Linearity, control effects, and behavioral types[END_REF], and contrasted these approaches with ours. In this section, we will contrast our work with the more recent work on manifest sharing [START_REF] Balzer | Manifest sharing with session types[END_REF].

Manifest sharing extends the session-typed language SILL with two connectives, ↑ S L A and ↓ S L A, which represent the places in a protocol where a shared resource is aquired and released, respectively. In the resulting language, SILL S , we can define a type for, e.g., shared queues (using the notation for types introduced in this paper):

queue A ::= ↑ S L ( A ⊥ ↓ S L (queue A) ) ( (A ⊕ ⊥) ↓ S L (queue A) )
The type queue A types a shared channel which, after we aqcuire exclusive access, gives us the choice between enqueuing a value (A ⊥ ) and releasing the queue, or dequeuing a value if there is any (A ⊕ ⊥) and releasing the queue. The language SILL S is much more expressive than HCP - ND , as it has support for both shared channels and recursion. In fact, Balzer, Pfenning, and Toninho [START_REF] Balzer | A Universal Session Type for Untyped Asynchronous Communication[END_REF] show that SILL S is expressive enough to embed the untyped asynchronous πcalculus. This expressiveness comes with a cost, as SILL S processes are not guaranteed to be deadlock free, though recent work addresses this issue [START_REF] Balzer | Manifest deadlock-freedom for shared session types[END_REF].

Despite the difference in expressiveness, there are some similarities between HCP - ND and SILL S . In the former, shared channels represent (length-indexed) streams of interactions of the same type. In the latter, it is necessary for type preservation that shared channels are always released at the same type at which they were acquired, meaning that shared channels also represent (possibly infinite) streams of interactions of the same type. In fact, in HCP - ND , the type for queues (with n interactions) can be written as ! n (A ⊥ (A ⊕ ⊥)).

One key difference between HCP - ND and SILL S is that in SILL S a server must finish interacting with one client before interacting with another, whereas in HCP - ND the server may interact with multiple clients simultaneously.

Discussion and Future Work

We presented HCP - ND , an extension of HCP -which permits non-deterministic communication without losing the strong connection to logic. We gave proofs for preservation, progress, and termination for the term reduction system of HCP - ND . We showed that we can define non-deterministic local choice in HCP - ND . Our formalism so far has only captured servers that provide for a fixed number of clients. More realistically, we would want to define servers that provide for arbitrary numbers of clients. This poses two problems: how would we define arbitrarily-interacting stateful processes, and how would we extend the typing discipline of HCP - ND to account for them without losing its static guarantees. One approach to defining server processes would be to combine HCP - ND with structural recursion and corecursion, following the µCP extension of Lindley and Morris [START_REF] Lindley | Talking bananas: Structural recursion for session types[END_REF]. Their approach can express processes which produce streams of A channels. Such a process would expose a channel with the co-recursive type νX.A (1 ⊕ X). Given such a process, it is possible to produce a channel of type A A • • • A for any number of As, allowing us to satisfy the type ? n A for an arbitrary n.

We would also need to extend the typing discipline to capture arbitrary use of shared channels. One approach would be to introduce resource variables and quantification. Following this approach, in addition to having types ? n A and ! n A for concrete n, we would also have types ? x A and ! x A for resource variables x. These variables would be introduced by quantifiers ∀xA and ∃xA. Defining terms corresponding to ∀xA, and its relationship with structured recursion, presents an interesting area of further work.

Our account of HCP -did not include the exponentials ?A and !A. The type !A denotes arbitrarily many independent instances of A, while the type ?A denotes a concrete (if unspecified) number of potentially-dependent instances of A. Existing interpretations of linear logic as session types have taken !A to denote A-servers, while ?A denotes A-clients. However, the analogy is imperfect: while we expect servers to provide arbitrarily many instances of their behaviour, we also expect those instances to be interdependent.

With quantification over resource variables, we can give precise accounts of both CP's exponentials and idealised servers and clients. CP exponentials could be embedded into this framework using the definitions !A ::= ∀n! n A and ?A ::= ∃n? n A. We would also have types that precisely matched our intuitions for server and client behavior: an A server is of type ∀n? n A, as it serves an unbounded number of requests with the requests being interdependent, while a collection of A clients is of type ∃n! n A, as we have a specific number of clients with each client being independent.

  (x[ ].x[ ]. | x(y). | x(z). ) =⇒ ( | { /y} | { /z}) or ( | { /y} | { /z})

  (x[ ].x[ ].x[ ]. | x(y). | x(z). | x(w). ) =⇒ ( | { /y} | { /z} | { /w}) or ( | { /y} | { /z} | { /w}) ( | { /y} | { /z} | { /w}) or ( | { /y} | { /z} | { /w})

  (( x[y]. | x[y ]. ) | x(z). x(z ). ) Γ, ∆, Θ

P

  G | Γ, y : A (? 1 ) x(y).P G | Γ, x : ? 1 A P G | Γ, x : ? m A, y : ? n A Cont ? P {x/y} G | Γ, x : ? m+n A

-

  νx.(( x[y].y inl.y[].0 | x[z].z inr.z[].0 ) | x(y). x(z).y {inl : (νw)(z {inl : z().w[].0; inr : z().w[].0} | w().P ) ;inr : (νw)(z {inl : z().w[].0; inr : z().w[].0} | w().Q) }) This term is a cut between two processes. On the left-hand side, we have a pool of two processes, x[y].y inl.y[].0 and x[z].z inr.z[].0. Each makes a choice: the first sends inl, and the second sends inr.

Non-determinism, Logic, and Session TypesRecent work extended πDILL and CP with operators for non-deterministic behaviour[START_REF] Atkey | Conflation confers concurrency[END_REF][START_REF] Caires | Types and logic, concurrency and non-determinism[END_REF][START_REF] Caires | Linearity, control effects, and behavioral types[END_REF]. These extensions all implement an operator known as nondeterministic local choice. (This operator is written as P + Q, but should not be confused with input-guarded choice from the π-calculus[START_REF] Milner | A calculus of mobile processes[END_REF].) Non-deterministic local choice can be summarised by the following typing and reduction rules:


Agustín E Martinez Suñé

Carlos G Lopez Pombo

Automatic Quality-of-Service evaluation in Service-Oriented Computing

Formally describing and analysing quantitative requirements of software components might be important in software engineering; in the paradigm of API-based software systems might be vital. Quantitative requeriments can be thought as characterising the Quality of Service -QoS provided by a service thus, useful as a way of classifying and ranking them according to specific needs. An efficient and automatic analysis of this type of requirements could provide the means for enabling dynamic establishing of Service Level Agreements -SLA, allowing for the automatisation of the Service Broker.

In this paper we propose the use of a language for describing QoS contracts based on convex specification, and a two-phase analysis procedure for evaluating contract satisfaction based on the state of the art techniques used for hybrid system verification. The first phase of the procedure responds to the observation that when services are registered in repositories, their contracts are stored for subsequent use in negotiating SLAs. In such a context, a process phase of contract minimisation might lead to great efficiency gain when the second, and recurrent, phase of determining QoS compliance is run.

Introduction

Distributed software resulting from paradigms like Service-oriented Computing -SOC, and emerging ones like Cloud/Fog computing and the Internet of Things are transforming the world of software systems in order to support applications able to respond and adapt to the changes of their execution environment, giving impulse to what is called the API's economy. The underlying idea of the API's economy is that it is possible to construct software artifacts by composing services provided by third parties and previously registered in repositories. This envisages a generation of applications running over globally available computational resources and communication infrastructure, which, at run-time, are dynamically and transparently reconfigured by the intervention of a dedicated Middleware with the capability to discover and bind a running application with a certain requirement, to a service capable of fulfilling it, subject to the negotiation of a Service Level Agreement -SLA, so they can collectively fulfill certain business goals [START_REF] Fiadeiro | An abstract model of service discovery and binding[END_REF].

Requirements have usually been classified in functional and non-functional depending on the nature of the attributes they capture. Functional requirements are usually understood as those describing what the system has to do, while nonfunctional ones generally express attributes that do not prescribe a particular behaviour but characterise how the system carries out the behaviour described by the functional ones. From non-functional requirements, we propose a further classification by identifying a subset referred to as quantitative attributes. We understand quantitative attributes as those that can be interpreted over a particular metric space [START_REF] Bryant | Metric spaces: iteration and application[END_REF]. This characteristic carries the potential of admitting some form of formal analysis, depending on the expressive power of the language used in specifying requirements over them. The reader shall note that not every metric space has associated formal methods of analysis but, from both practical and theoretical point of view, the real numbers constitute a natural candidate over which many quantitative attributes can be interpreted. As usual, requirements can be used as contracts between software components and satisfaction of such contracts is dealt with by checking whether certain judgement of the form Pr Rq holds or not, where Pr is the provision contract and Rq is the requirement contract.

From this perspective, those quantitative non-functional requirements formalised over attributes interpreted as real variables might be used to classify functionally equivalent services by the Quality of Service -QoS they provide. This means that while services might have the same functional behavior, they could differ on their non-functional one (for example, a service may offer low speed computation at a very low cost while another, functionally equivalent one, might be faster but more onerous), a phenomena that could be useful as a way of classifying and ranking them according to specific needs; a motivation shared with other works like [START_REF] Strunk | QoS-aware service composition: A survey[END_REF].

Identifying and formally describing quantitative properties of a system is not novel, examples of this range from the well known formalisation of the time/space required by an algorithm by means of the asymptotic growth of functions [2, Part. I, Chap. 2], to a very prolific research field dedicated to the verification of hybrid systems. Hybrid systems [START_REF] Henzinger | The theory of hybrid automata[END_REF] are dynamic artifacts exhibiting both discrete and continuous behaviour. In general, the continuous aspects of such systems are formalised as constraints over variables taking their values from the real numbers. There is a plethora of analysis techniques that have been proposed for this type of systems, with the vast majority focussing on those aspects laying within the boundary of what is decidable [START_REF] Henzinger | What's decidable about hybrid automata[END_REF]. A relatively new approach to the analysis of hybrid systems' specification, due to Pappas et al. [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF], integrates SMT-solving [START_REF] De Moura | Satisfiability modulo theories: introduction and applications[END_REF] with convex constraints [START_REF] Grünbaum | Convex polytopes[END_REF], under the name of SMC -Satisfiability Modulo Convex Optimization.

In this work we developed an efficient two phase procedure for evaluating quantitative SLA based on SMC, but adapted to profit from the fact that contracts (both provision Pr and requirement Rq) can be minimised in a preprocessing phase, referred to as Minimisation through Convex Optimisation -MCO, when the service is registered in the repository. The expectation is that such preprocessing might produce an efficiency gain when Pr Rq is checked to evaluate if an SLA is met. Moreover, as finding the minimum size contract requires, at least, enumerating all boolean assignments satisfying a SAT problem, we propose an approach in which contract minimisation can be performed as semantics preserving incremental partial minimizations.

The paper is organised as follows: in Sec. 2 we concentrate both the definition of the formal framework we will use to specify QoS contracts as quantitative requirements, and present our proposal for its analysis, at the same time we state the research questions we want to answer; in Sec. 3 we present the experimental design and results supporting the answers to each of the research questions. Finally in Sec. 4 we draw some conclusions and point out some further lines of research.

Formalisation and analysis of QoS contracts

In this section we concentrate on formalising QoS contracts by identifying quantitative non-functional requirements and, in analogy to the continuous elements in hybrid system specification, by interpreting each of the attributes as a real variable. Thereafter, we present state of the art analysis techniques for this kind of formal specifications and our proposal for the optimisation of the procedure based on a preprocess of contract minimisation.

In [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF], Pappas et al. adopt monotone SMC formulae as specification language; we will refer to this specifications as convex specification. Monotone SMC formulae are defined as quantifier-free formulae in conjunctive normal form, with atomic propositions ranging over a subset of the propositional variables and convex constraints.

Definition 1 (Convex specification, Sec. 3.2, [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF]). Let X be a set of real variables and P a set of propositional variables, then a monotone SMC formula is any formula that can be produced by the following grammar: , where f is an affine function and x 0 , . . . , x arity(f ) ∈ X . inequality ::= f (x 0 , . . . , x arity(f ) ) relation 0

, where f is a convex function and x 0 , . . . , x arity(f ) ∈ X . relation ::= < | ≤ Then a convex specification over X and P is a tuple X , P , α , where α is a monotone SMC formula over X and P.

In the grammar above, affine function and convex function denote, as one could guess, affine and convex functions, respectively. Monotone SMC formulae only admit convex constraints as atoms, in contrast to generic SMC formulae over convex constraints [START_REF] Nuzzo | CalCS: SMT solving for non-linear convex constraints[END_REF], reverse convex constraints are not allowed3 . As it is mentioned in [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF], monotonicity (i.e. the lack of negation to convex constraints) is key to guarantee that whenever a convex specification has a model, it is found by solving one (or more) convex optimization problems.

The following example illustrates a specification written in the language presented in Def. 1.

Example 1 (Service requirement). Let us consider a context of an API-based software application requiring a service accessed and paid for, for the time it is used. In that context we consider as relevant quantitative attributes the cost (formed by: a. perSec: the cost (in a given currency) of the service per second elapsed while the communication session is open, and b. costMb: the cost (in the same currency) per megabyte of information processed); and execution time (formed by: a. maxWait: the maximum waiting time in seconds for the server to effectively attend a request, b. maxTimeGb: the maximum amount of time in seconds the service will execute for processing one gigabyte, and c. netSpeedMb: an upper bound in seconds for transferring one megabyte). Additionally, costs may change if the system requiring the service has some kind of promotional code. Then, such attributes can be formalised by a convex specification X , P , α where X = {perSec, costMb, maxWait, maxTimexGb, netSpeedMb}, P = {promotionMode}, and where α is the conjunction of the following formulae4 :

0 < maxWait ≤ 100 (1000 ≤ maxTimexGb ≤ 3000) ∧ (0.05 ≤ netSpeedMb ≤ 0.15) promotionMode =⇒ 0.0 ≤ perSec < 0.1 ¬promotionMode =⇒ 0.1 ≤ perSec ≤ 0.3 costMb < 0.5
In [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF]Def. 3.4] the authors define the monotone convex expansion of a convex specification X , P , α as a new convex specification X , P , α where:

-P = P ∪ V, where V = v f ( → x ) R 0 | f ( → x ) R 0 appears in α and -α = α B ∧ v C ∈V (¬v C ∨ C) , where α B = α | v C
C , the result of substituting every occurrence of an affine/convex constraint C in the monotone SMC formula α by the fresh new propositional variable v C ∈ V associated to C, called the propositional abstraction of α.

Thereafter, in [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF]Prop. 3.5], the authors prove that: 1. α and α are equisatisfiable (i.e. for every satisfying assignment for α, there exists a satisfying assignment for α) and if α is unsatisfiable, then so is α, 2. any satisfying boolean assignment for α B reduces the satisfiability problem of α to a conjunction of convex constraints, and 3. the satisfiability problem of α reduces to a finite disjunction (one for every satisfying boolean assignment for α B ) of finite conjunctions of convex constraints.

Roughly speaking, the analysis method proposed by Pappas et al. in [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF], sketched in Fig. 1, reduces to enumerating every possible satisfying boolean assignments γ : P → {0, 1} for α B , and then using a convex constraint solver for testing the feasibility of the set of convex constraints {C | γ(v C ) = 1}.

1. Let X , P , α be a convex specification and αB the propositional abstraction of α, and a function δ mapping variables in V to their corresponding convex or affine constraint appearing in α, 2. Feed an SAT-solver with αB, 3. if there exists a satisfying assignment γ, then 1. Feed a convex solver with {f

( → x ) R 0 | (∃v ∈ V)(δ(v) = f ( → x ) R 0 ∧ γ(v) = 1)} 2. if it is feasible then 1. α is satisfiable else 2.
Update the SAT-solver information with ¬minimise(γ δ ) 3. goto 3, 4. α is unsatisfiable Fig. 1: SMCO analysis procedure Updating the SAT-solver's clause database by injecting a new clause, as it is done in Line 3(2)2 requires the next assignment to satisfy the clauses in SAT-solver database, plus the new one. Minimising an assignment γ V (the subassignment of γ considering only variables in V), as stated also in Line 3(2)2, produces a clause γ min

V (subassignment of γ V such that {C | γ min (v C ) = 1})
which is (potentially) smaller that γ V , minimal and still unfeasible. It is reasonably evident that the smaller the amount of variables involved in γ min V , the bigger the pruning of the search space, because no boolean assignment containing such partial assignment will be considered further in the enumeration of satisfying boolean assignments. We will return to this point in Sec. 3 where we discuss some implementation notes. It is worth noting that clause minimisation, used to produce more efficient unsatisfiability certificates during the enumeration of satisfying boolean assignments, is orthogonal to the main contribution of this work on the minimisation of QoS contracts. This type of automatic analysis is usually understood as a refutation method aiming at finding counterexamples to properties. Assume X , P , α is a sat-isfiable5 convex specification of a system and β a desirable property written in the same language then, if α ∧ ¬β (a formula equivalent to ¬(α =⇒ β)) is satisfiable, one can conclude that β does not follows from α, and the satisfying assignment constitutes a counterexample.

From QoS contracts to an efficient determination of SLA

Service-Oriented Computing relies on a notion of software system as a dynamic entity built up from services discovered and bound in run-time. To make this possible, services must be previously registered in public repositories from where they can be procured by a Service broker as required by a dedicated Middleware who dynamically reconfigures the executing application by binding it to the service. This process of dynamic reconfiguration is triggered automatically by an application reaching a point in its execution where a continuation depends exclusively on the intervention of an external service.

Consider the case of a (satisfiable) QoS requirement contract Rq. A service with a (satisfiable) QoS provision contract Pr will be a good candidate only if Pr =⇒ Rq holds; or equivalently, the formula Pr ∧ ¬Rq is not satisfiable. Assuming that such a formula can be seen as a convex specification (i.e. a formula that can be produced by the grammar in Def. 1), then it is possible to perform the interoperability check by executing the algorithm of Fig. 1 to determine compliance between the application's QoS requirement contract and the service's QoS provision contract. Although from a theoretical point of view there is no objection to applying this procedure for determining SLA, from a practical perspective, this interoperability check is expected to be performed over many candidates, in order to guarantee that the service chosen by the service broker is the optimum according to the status of the repository.

Such a use context imposes strong efficiency considerations over this type of analysis, and coping with them requires reducing the execution time for performing the analysis as much as possible, even at the expense of investing a bigger amount of time preprocessing the contracts in advance when the services are registered in the repository. Returning to our example, assume that Pr and ¬Rq are satisfiable convex specifications denoting provision QoS contract and the negation of a requirement QoS contract, respectively; both Pr B and ¬Rq B might have plenty of satisfying boolean assignments γ Pr (resp. γ ¬Rq ) leading to non-feasible sets of convex constraints

{C | γ Pr (v C ) = 1} (resp. {C | γ ¬Rq (v C ) = 1}
), suggesting that contracts admit some relative minimisation that can be performed by updating the solver's clause database by injecting a new clause characterising such unfeasibility information. Ideally this process of Minimisation through Convex Optimisation -MCO must traverse the whole space of boolean assignments of the propositional abstraction of the contract, determining which of them leads to a feasible set of convex constraints. This observation motivates the idea of a two phase analysis approach based on the algorithm of Fig. 1, in which the first phase aims at the minimisation of QoS contracts, performed only once when a service is registered in a repository, and the second phase is the analysis of QoS contract compliance, executed for SLA negotiation.

A two phase analysis algorithm of convex specifications Our proposal for the analysis of QoS contract compliance is motivated by the specific usage scenario of SOC, where specifications are expected to be reused in many analysis. Such a context imposes that time consumption to check whether Pr ∧ ¬Rq is satisfiable or not, has to be as tight as possible due to the fact that such a check has to be performed over every candidate satisfying the functional requirements.

To cope with such demand, we devised a preprocess (referred to as minimisation phase) aiming at the minimisation of QoS contracts, represented by a convex specification, and a second phase (referred to as check phase) that implements the exact same analysis than the algorithm of Fig. 1.

Our first research questions aims at relating the performance of the algorithm in Fig. 1 as distributed by Pappas et al. and our reimplamentation when satisfying boolean assignments are iterated by using Z3 and Minisat as SAT-solvers.

RQ1: Is there any performance gain in a Z3-based implementation of the check phase with respect to that of the algorithm shown in Fig. 1? What about between a Minisat-based implementation with respect to the Z3-based implementation of the check phase?

Next we present and evaluate the main contribution of the paper, being the implementation of a QoS contract MCO procedure, aiming at preprocessing QoS contracts in order to prune a significant portion of the space of satisfying boolean assignments of its propositional abstraction. Such minimisation procedure is motivated by two observations about the algorithm of Fig. 1: 1. the analysis procedure relies on enumerating all possible models of the propositional abstraction of the QoS contract, and 2. line 3(2)2 of the algorithm of Fig. 1 alters the enumeration process by using the unfeasibility information obtained from the convex analysis, transformed into a minimal boolean clause, acting as an unfeasibility certificate. The algorithm for QoS contract MCO is based on performing convex analysis to test the feasibility of the set of convex constraints determined by each satisfying boolean assignment. The single difference with SMCO analysis procedure is that, while in Line 3(2)1 of the algorithm of Fig. 1 the problem is reported as satisfiable and the search for more satisfying assignments ends, MCO discards that satisfying boolean assignment to return to the enumeration and continue the search for boolean assignments that lead to non-feasible sets of constraints.

Given a QoS contract, consisting of a monotone SMC formula α, the reader might note that the minimisation process visits all satisfying boolean assignments of the propositional abstraction α B in order to determine which of them are declared feasible by the convex solver so they must remain as satisfying boolean assignments, and which of them must be pruned from the space of models of the specification. Then we can design a two phase convex analysis algorithm by considering: 1. a single time application of the process of QoS contract MCO phase of both, a provision contract Pr , and the negation of a requirement contract ¬Rq, yielding Pr and ¬Rq respectively, and 2. a second phase of searching for a satisfying boolean assignment for the propositional abstraction of Pr ∧ ¬ Rq that leads to feasible set of convex constraints (i.e. the result of applying the algorithm shown in Fig. 1).

An important concern regarding the MCO procedure, is that, as we mentioned before, minimising a QoS contract requires visiting all possible boolean assignments satisfying the propositional abstraction of the formula Pr ∧ ¬ Rq. It is trivial to see that this procedure is of an exponential nature due to the fact that the size of the space of satisfying boolean assignments of a boolean formula is (potentially) exponential with respect to the amount of boolean variables 6 . Having said that, efficiency improvement resulting from potential optimisations of the process cannot change such a high complexity bound. A direct consequence of this observation is that, even if minimisation is considered as a one time preprocess, full scalability is, by any means, unreachable.

The remaining research questions aims at evaluating the performance of our proposal of a two phase procedure for checking QoS contract compliance. To accomplish that, the comparison of the three different implementations of the SMCO analysis procedure done to answer RQ1 will serve to set a baseline for the experimental evaluation of the main contribution of this work, being the comparison of the time required for checking QoS contract after performing a Minimization Through Convex Optimisation phase.

The second research question aims at identifying whether there is a bound to the size of the QoS contracts that can be fully minimised.

RQ2: What is the size of QoS contracts that can be fully minimised in 3 hs.?

A close look to the proposed minimisation procedure exposes that if it were stopped at any iteration, right before continuing the enumeration of satisfying boolean assignments, the resulting QoS contract shares every feasible model with the original one.

Proposition 1. Let X , P , α be a convex specification, α B the propositional abstraction of α and δ a function mapping variables in V to their corresponding convex or affine constraint appearing in α. Let [α B i ] 0≤i≤n be a sequence of boolean formulae where α B 0 = α B , α B i+1 , for all i < n -1, is the result of a single iteration of the minimisation algorithm to α B i and α B n is the result at the end of the algorithm.

Then, every convex specification X , P , α B i , where 0 ≤ i ≤ n, share the same feasible models.

An interesting fact derived from the previous proposition is that the process of QoS contract minimisation can be performed incrementally, one iteration at a time, leading to a succession of partially minimised QoS contracts, leading us to our third research question.

RQ3: How does the nature of the problem change considering successive partial minimisations of a given specification?

Implementation and experimental results

In this section we present the answers to the research questions posed in Sec. 2 through experimental evaluation. First we will provide some details about the implementation of the algorithms, the hardware configuration of the experimental setup and the dataset used for the experimental evaluation.

Notes on the implementation In this section we will briefly discuss some aspects of the implementation of the algorithms presented in the paper. The implementation developed by Pappas et al. in [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF] of the algorithm of Fig. 1 uses Z3 [START_REF]Z3: An efficient smt solver[END_REF] as SAT-solver. Having said that, we developed two versions of our algorithms, one also using Z3 to check wheter the reimplementation of the algorithm does not introduce any significant difference in performance, a second one resorting to Minisat [START_REF] Eén | An extensible sat solver[END_REF], a well-known SAT-solver whose minimality has made it one of the most efficient ones available.

Checking feasibility of sets of constraints was implemented using IBM ILOG CPLEX Optimization Studio [START_REF]IBM: IBM ILOG CPLEX Optimization Studio[END_REF] since it is one of the most powerful convex optimization softwares that is available for research and educational purposes.

The algorithm orchestrating the enumeration of satisfying boolean assignments of the propositional abstraction of the contracts with the convex solving of the set of convex constraints determined by corresponding assignment, as well as all the framework needed for the generation of instances according to the experimental design and their systematic execution were developed in Python 2.7 (https://www.python.org) resorting to the existent libraries needed to integrate the various tools mentioned above.

Hardware configuration Experiments were run over an x86 64 architecture processor Intel(R) Core(TM) i5 CPU 750 at 2.67GHz (CPU MHz: 2661 -CPU max MHz: 2661 -CPU min MHz: 1197) with 3 level cache (L1d cache: 32K, L1i cache: 32K -L2 cache: 256K -L3 cache: 8192K), 8 Gb of SDRAM at 1333 MHz, and running SMP Debian Linux 4.9.88-1+deb9u1 (2018-05-07). Each individual instance was run for at most 3 hours, unless it is noted, as we believe that what is feasible within that time frame provides enough information to validate our answers. Whenever the analysis of a problem instance, or the construction of the solving infrastructure, exceded the time limit, the corresponding cell in the tables was marked with "TO" denoting that the process reached the timeout, and whenever the limit was a consequence of the exhaustion of the system memory leading the machine to a sate of trashing was marked with "OoM" denoting the system run out of memory.

Notes on the experimental setting A first note on the experimental designs we need to put forward is that we did not use the experimental setting distributed by the authors of [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF] for the following reasons: 1) specifications are constructed hardcoding the solver instance and not providing any interface allowing users to feed a specification in any standard language, making very difficult to test the tool over different data sets, and 2) there is no report on the time needed to construct the solver instance which, after profiling the implementations based on Z3, are proven to be not negligible due to the fact that part of the solving is performed during the addition of the clauses, sometimes consuming more time than the invocation of the solve itself (see column "Initialisation time" of Table 1).

Experimental evaluation

In this section we evaluate the research questions posed previously and show experimental data supporting our answers.

RQ1: Is there any performance gain in a Z3-based implementation of the check phase with respect to that of the algorithm shown in Fig. 1? What about between a Minisat-based implementation with respect to the Z3-based implementation of the check phase?

Experimental design: QoS provision contracts were obtained by first generating random SAT instances of satisfiable provision contracts, Pr B using the number of boolean and real variables as parameters. The dataset is formed by QoS contracts with boolean variables ranging from 50 to 350, stepping every 50 variables. The number of clauses is 80 times the number of boolean variables. From the total amount of variables we randomly choose 50% to which we associated randomly generated linear convex constraints. Convex constraints were considered to apply over 5 to 30 real variables stepping every 5 variables. Satisfiable contracts ¬Rq B are obtained from: 1) negating Pr B , 2) pushing negations to the atoms, and 3) reversing the linear constraints (producing also linear constraints). In this way, Pr B ∧ ¬Rq B results satisfiable from the boolean point of view, but having no feasible convex model. This lack of counterexamples for Pr =⇒ Rq aims at stressing the checking procedure forcing it to traverse the whole space of solutions.

The upper limit in the number of boolean variables respond to the fact that generating a CNF boolean formula ¬Pr B as a QoS requirement contract, using Tseitin's transformation [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF], yields a boolean formula quadratically bigger than Pr B , both in the number of clauses and variables. If we consider that a propositional abstraction of a provides contract Pr B of 400 boolean variables and 32000 clauses results in a 35 Mb file, the construction of a QoS contract equivalent to ¬Pr B yields a CNF formula of approximately 30000 boolean variables and 9500000 clauses, consuming approximately 1 Gb. The analysis was performed over 8 instances of each combination of boolean variables and real variables to try palliating the variance among cases. The time was split in two, the time needed to setup the checking infrastructure, and the analysis time itself, as the use of Z3 showed that a significant part of the analysis takes place during the initialisation of the SMT-solver with the clauses.

Experimental results: Table 1 shows the running time comparison between the original implementation of SMCO algorithm presented [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF], reviewed in Fig. 1, and the implementations of the check phase based on Z3 and Minisat. The layout of the table is: 1. the first column shows the amount of boolean variables in the provision contract, 2. the second one shows the solver used to solve the problem, 3. the third column shows the time required for initialising the solver until the exact moment before it is ready to solve the problem, and 4. columns fourth to nine show the average time required to solve the instances of the corresponding number of real variables. Figure 2 Conclusions and discussion: Observing the running times obtained from executing the three implementations of SMCP algorithm for checking an unsatisfiable formula shown in Table 1 we derive the following conclusions: 1. running time grows exponentially at a rate of 2.37 on the number of boolean variables, 2. serving the rows it is possible to appreciate that the time required to analyse the satisfiability of the instances grows until it finds a maximum, then decrease until it stabilises in what seems to be a plateau. As for every row the CNF used is the same, also prescribing the amount of convex constraints, this phenomenon seems to expose a relation between the number of constraints and the number of real variables over which those constraints are expressed. It is also observable that decrease, and further stabilisation, of the time is mimicked by the number of iterations of the algorithm. Having said this, we believe that understanding this particular phenomenon has no impact on the experiment conducted to answer this research question, 3. there is no consistent and significant difference between the performance of the SMCP original implementation by Pappas et al. and our implementation based on Z3 as boolean solver. The experimental data shows a running time difference no bigger than 10%. This difference might be a byproduct of having developed a more abstract implementation of the convex specification encapsulating an iterator for the satisfying boolean assignments of the propositional abstraction, 4. the Minisat-based implementation greatly outperforms both Z3-based implementations taking only approximately 2% of the time required by the latter, considering setting up the analysis infrastructure and analysing compliance altogether.

An important observation about the answer given to RQ1, is that only the Minisat-based implementation of the check phase algorithm can produce a significant amount of experimental data useful enough to evaluate our proposal of a two phase QoS contract compliance analysis procedure; thus RQ2 and RQ3 will be answered only evaluating the performance of the Minisat-based implementation of both phases of the procedure.

RQ2: What is the size of QoS contracts that can be fully minimised in 3 hs.?

Experimental design: The dataset used to run the experiment was generated using the same criteria used for generating the dataset used to run the experiment performed to answer RQ1 but considering a finer granularity in the axis of boolean variables (stepping every 5) and starting from 30 variables, as the running time of the minimisation phase of instances with less than 30 was negligible. In those cases in which the minimisation process did not find any unfeasible convex model thus, not producing any minimisation, the running time is reported tagged with (nm), indicating "no minimisation". Conclusions and discussion: Results shown in Table 2 expose that a naïve approach to minimisation is not viable as the cost of full minimisation might be too high, even for very small contracts.

Experimental results:

RQ3: How does the nature of the problem change considering successive partial minimisations of a given specification?

Experimental design:

To provide an answer to this research question we performed partial minimisations (from 0 minutes to 3 hours stepping every 30 minutes) of every pair of QoS contracts of those cells of rows 200, 250 and 300 of Table 1 where the number of real variables ranges between 5% and 10% of the number of boolean variables. Then, we performed the compliance analysis in order to identify how analysis time decreases while more time is invested in the minimisation procedure.

Results: Figure 3 show graphs of the evolution of time required by the check phase over partially minimised QoS contracts, considering the snapshots taken every 30 minutes of minimisation. Table 3 shows the comparison of the solving Conclusions and discussion: Observing the graphs in Fig. 3 we derive the following conclusions: 1. the running time required by the check phase decreases while the amount of time invested in minimisation grows. For QoS contracts over 200 boolean variables, the time required by the check phase drops dramatically to a plateau after only 30 min. of minimisation. In the case of QoS contracts over 250 boolean variables, the pattern is exactly the same but requiring between 60 to 90 min. of minimisation. Finally, for QoS contracts over 300 boolean variables, this phenomenon can be seen only for instances over 25 real variables after 150 min. but in the case of 30 real variables we can witness cases that cannot be checked within 3 hs. time when QoS contracts are not minimised, that can be checked after 60 min. of minimisation phase, 2. the growth on the number of real variables for instances over the same number of boolean variables shows more dispersion (in the time required for the check phase) over instances minimised for short periods of time, but rapidly collapsing to the plateau, The results in Table 3 show how 3 hs. of minimisation phase dramatically reduce the cost of the check phase. The reduction naturally depends on the size of the problem under analysis; it is easy to see that bigger problems show smaller reductions over the same amount of time invested in the minimisation phase.

Conclusions

We proposed the use of a formal language for QoS contract specification together with an associated two phase compliance checking procedure, based on the algorithm proposed by Pappas et al. in [START_REF] Shoukry | SMC: Satisfiability modulo convex optimization[END_REF] for hybrid system verification, adapted to the concrete scenario of SLA negotiation for the automatic reconfiguration of software systems found in distributed environments such as SOC.

Research questions were posed and experiments were conducted to answer them. The dataset was designed in order to stress the technique by forcing the problem instances to be unsatisfiable thus, requiring the exhaustion of the space of potential solutions; the evaluation of the tool under satisfiable instances remains to be addressed. The experimental results shown in the answering of RQ2 evidenced that full minimisation of contracts might be unreachable as time and memory consumption, even for small case studies, result too high. To mitigate such demand we proposed the use of incremental minimisation and the experimental results shown in the answering of RQ3 evidenced that a relatively small amount of time invested in a first phase of QoS contract MCO dramatically reduces the time required by a second phase dedicated to check compliance of minimised versions of the QoS contracts.

  Carlos G. Lopez Pombo's research is supported by Universidad de Buenos Aires by grant UBACyT 20020170100544BA, and Consejo Nacional de Investigaciones Científicas y Técnicas by grant PIP 11220130100148CO. The authors want to thank to Marie Sk lodowska-Curie Research and Innovation Staff Exchange BehAPI -Behavioural Application Program Interfaces.

  formula ::= {clause ∧} * clause clause ::= ({literal ∨} * literal ) literal ::= p | ¬p | | ⊥ | conv constraint , where p ∈ P conv constraint ::= equation | inequality equation ::= f (x 0 , . . . , x arity(f ) ) = 0

  show the running time of the tool using the algorithm in Fig.1and the Z3-based implementation of the check phase algorithm, while Figs.2c and 2dshow the running time using the Minisat-based implementation. (a) 50 boolean vars. in provides using Z3 (b) 100 boolean vars. in provides using Z3 (c) 50 bool. vars. in provides using Minisat (d) 100 bool. vars. in provides using Minisat

Fig. 2 :

 2 Fig. 2: Compliance analysis of QoS contracts over 50 and 100 boolean variables in provides (total problem size of +4000 and +8000 bool. vars. respectively)

Fig. 3 :

 3 Fig. 3: Solving times for partial minimisations (from 0 minutes to 3 hours stepping every 30 minutes) of provides and requires QoS contracts

Table 1 :

 1 shows boxplots graphs containing the run-Comparison of different implementations of algorithm for checking an unsatisfiable formula time information for the first two rows of Table1exposing the relative stability of the algorithms. Figures2a and 2b

	# bool. vars		Initialisation			# real variables
	in provides	Solver	time (approx.)	5	10	15	20	25	30
		SMC	150 157.48 176.71 176.71 178.28 176.86 178.22
	50	Z3 check	170 167.82 177.82 177.55 177.01 176.84 177.55
		Minisat check	4	3.21	2.23	2.13	2.12	2.12	2.12
		SMC	630 1575.70 1802.20 1756.17 1812.62 1854.42 1852.64
	100	Z3 check	640 1589.20 1819.81 1843.83 1954.84 1925.89 1931.48
		Minisat check	17	16.47	19.89	11.90	10.01	9.11	8.70
		SMC	1680 4243.10	TO	TO	TO	TO	TO
	150	Z3 check	1820 4580.25	TO	TO	TO	TO	TO
		Minisat check	45	21.32 174.12	79.92	47.76	26.66	23.60
		SMC	3100	TO	TO	TO	TO	TO	TO
	200	Z3 check	3120	TO	TO	TO	TO	TO	TO
		Minisat check	77	35.53 236.32 906.17 488.88 102.78	60.34
		SMC	4920	TO	TO	TO	TO	TO	TO
	250	Z3 check	5010	TO	TO	TO	TO	TO	TO
		Minisat check	127	45.93 321.73 1231.22 2929.81 1052.29 405.59
		SMC	OoM	-	-	-	-	-	-
	300	Z3 check	7300	TO	TO	TO	TO	TO	TO
		Minisat check	186	60.05 431.87 1714.84 4423.42 8259.39 4720.92
		SMC	OoM	-	-	-	-	-	-
	350	Z3 check	OoM	-	-	-	-	-	-
		Minisat check	OoM	-	-	-	-	-	-

  Table 2 shows the running time of the minimisation phase. A side by side comparison of the time required by the analysis algorithm, over

				# real variables
	# boolean vars	5	10	15	20	25	30
	30	186.68 (nm) 200.40	(nm) 203.18 (nm) 206.43	(nm) 209.94 (nm) 212.82
	35	691.26 (nm) 852.93	(nm) 921.20 (nm) 930.37	(nm) 944.27 (nm) 953.85
	40	5606.34 (nm) 9519.08 (nm) 9682.34 (nm) 9814.39 (nm) 10004.27 (nm) 7234.67
	45	TO TO	TO	TO	TO	TO

Table 2 :

 2 Running time of the Minisat-based minimisation algorithm minimised and not minimised instances, is of no interest in this case as the cost associated to the process of full minimisation of QoS contracts is so high that even the smaller instance of Table1of 50 boolean variables and 5 real variables could not be minimised within the time bound of 3 hs.

Table 3 :

 3 Comparison of solving time required between not minimised and minimised contracs(3 hs.)

Note that linear convex constraints could admit negations but, as the negation of a linear convex constraints can be rewritten as a linear convex constraint itself, there is no need for any special treatment.

The reader shall note that there is no impediment in translating the specification below to a formula recognisable by the grammar presented in Def. 1.

It is important for the specification to be satisfiable in order to ensure the existence of logical models, which in the case of this particular language, are boolean assignments. The existence of a model can be interpreted as the existence of a concrete implementations of the system satisfying the specification.

To be precise, the problem of enumerating all possible satisfying assignment of a SAT-formula is, at least, in the complexity class #P.


Miguel Abambres
email: abambres@netcabo.pt

Tiago Ribeiro

Ana E Sousa

Eva Lantsoght
email: l.lantsoght@tudelft.nl

Research Counts, Not the Journal

Keywords: Scientific Papers, Impact Factor, Indexing Databases, Research Quality, Scientific Performance, Scientometrics

Introduction

The Journal Impact Factor (JIF), today calculated by Clarivate Analytics (previously intellectual property of Thomson Reuters), was originally proposed by Irving H. Sher and Eugene Garfield in 1963 [START_REF] Garfield | The history and meaning of the journal impact factor[END_REF] as a tool to help librarians identify journals worth purchasing; not as a measure of the research quality in an article. The JIF is computed in each annual issue of the Journal Citation Reports (JCR, an annual publication by Clarivate Analytics), and represents the average number of citations per article in that year, concerning only papers published in that journal in the last two years: # WoS citations in year to papers published in years ( -1) and ( -2) # papers published in years ( -1) and ( -2)

year n n n n JIF nn = , (1)
where '# WoS citations' is the number of citations from articles published in journals indexed in Web of Science (WoS) database.

The number of inbound citations in the JCR only takes into account citing sources indexed in the WoS database. A similar metric is the 5-year impact factor (IF), which is calculated alike the former, but based 2 on five years (instead of two) prior to the JCR year. Citing Clarivate Analytics [2]: "the JIF is a journal-level metric, thus it does not apply to individual or subgroups of papers published in the journal, nor to authors of papers, research groups or institutions." Even so, it´s well-known in the scientific community that the JIF has increasingly become a means of judging the scientific quality of a journal and of everything that is published in it [START_REF] Eston | Editorial: The Impact Factor: a misleading and flawed measure of research quality[END_REF][START_REF] Quan | Publish or impoverish: An investigation of the monetary reward system of science in China (1999-2016)[END_REF].

According to Pudovkin [START_REF] Pudovkin | Comments on the Use of the Journal Impact Factor for Assessing the Research Contributions of Individual Authors[END_REF], and confirmed by the authors, there is extensive literature criticizing the JIF (mis)uses. The main argument against the use of JIF for characterization of individual papers and scientists is a lack of strong correlation between its value and the citedness of the individual papers published in the journal. There is no guarantee that an article published in a high IF journal will attract profuse citations [START_REF] Ranjan | Bibliometric Indices of Scientific Journals: Time to overcome the obsession and think beyond the Impact Factor[END_REF]. It is known [START_REF] Robert | Impact factor: The holy grail of research[END_REF] that only a fraction of the papers published in a high IF journal receive most citations contributing to the JIF, regularly known in scientometrics as the 'invitation's paradox' [START_REF] Vinkler | Introducing the Current Contribution Index for characterizing the recent, relevant impact of journals[END_REF]. By the end of the last century, Seglen [START_REF] Seglen | Why the impact factor of journals should not be used for evaluating research[END_REF] reported that 15 and 50 per cent of the most cited papers account for 50 and 90 percent of the citations used to compute the JIF, respectively. Moreover, (i) information abounds about classic highly-cited papers that were initially rejected by high IF journals [START_REF]Coping with peer rejection[END_REF]11], and (ii) data from several lines of evidence suggest that the reliability of scientific experiments decreases with increasing JIF [START_REF] Brembs | Prestigious Science Journals Struggle to Reach Even Average Reliability[END_REF].

This manuscript presents a critical overview on the use of the journal impact factor and/or journal indexing information for the scientific performance assessment of a researcher. The authors present a research-based opinion article, which addresses a serious problem that, in our opinion, remains fully topical until it is solved. Particularly, Figures 1234567partially illustrate interviews given by Nobel Laureates on this topic. Lastly, complementary and alternative versions of the JIF are proposed, respectively called Complementary (CIF) and Timeless (TIF) Impact Factors, aiming to better assess the average quality of a journal -never of a paper or an author. The idea behind impact factors is not useless; it has just been misused. The authors believe that in the ever-evolving landscape of science, it is necessary to keep the discussion going and to keep searching for improvements.

The JIF and indexing information as individual research quality measures

Deans, sponsors, government agencies and employment panels use the JIF as a convenient, yet flawed, performance measure [START_REF] Abbasi | Let's dump impact factors[END_REF]. According to Pudovkin's 30-year experience [START_REF] Pudovkin | Comments on the Use of the Journal Impact Factor for Assessing the Research Contributions of Individual Authors[END_REF] as a member of research staff recruitment committees at the institute of Marine Biology and the Russian Academy of Sciences, members in those committees typically just look at the journal titles. In many Universities in non-English-speaking countries, only papers published in WoS-indexed journals count towards merit [START_REF] Smeyers | How to Improve your Impact Factor: Questioning the Quantification of Academic Quality[END_REF]. The authors of this article oppose these types of judgement and support the opinions shared by many scientists as presented in the next section. In what follows, several examples are given of countries and institutions supporting these types of (mis)evaluation.

Instituto Superior Técnico, one of the most renowned schools of engineering and technology in Portugal (the only Portuguese member of the CLUSTER -Consortium Linking Universities of Science and Technology for Education and Research [START_REF] Cluster | Members -CLUSTER[END_REF]), part of the University of Lisbon, considers the journal impact factor quartiles published in WoS and/or Scopus databases to compute a quantitative measure of the scientific performance of its faculty staff (as described in chapter II, article 17 of UL [START_REF]Reitoria -Despacho n.º 3855/2017[END_REF]) -papers from journals in the 1st (Q1), 2 nd or 3 rd quartiles are given six, four or two times higher classification than the Q4 3 counterpart, respectively. Instituto Superior Técnico is also known, at least in some departments, for disregarding or giving much less credit to articles not published in Q1/Q2 WoS-(e.g., UL 2017b, d [START_REF]Edital[END_REF][START_REF]Edital[END_REF]) or Scopus-(e.g., [START_REF]Edital[END_REF]) indexed journals when assessing candidates for faculty positions in public tenders.

Ostravská univerzita v Ostravě [START_REF] Ostravská Univerzita V Ostravě | Open position for a postdoctoral fellow[END_REF] shows an example in the Czech Republic of a job application requiring a list of publications in WoS-indexed journals and the number of citations provided by that database, meaning that what matters the most is not the content of the publications, but where they are indexed. Furthermore, the inbound citations 'from journals' not indexed in WoS are of no value for that evaluation committee.

Spanish law rewards the researchers for publishing in journals that are deemed 'prestigious' by WoS (Q1, Q2, Q3) [START_REF] Muthamilarasan | Impact of impact factor in quantifying the quality of scientific research[END_REF].

In Brazil, the evaluation of graduate programs relies heavily on JIFs. Journals and their papers are classified within seven categories with decreasing IF ranges (A1, A2, B1, B2, B3, B4, C), known as the 'Qualis System' [22]. In 2001, the Brazilian ministry of science and technology created a program to affiliate ten promising young doctorates to research centers. In the same year, the Brazilian national research council (CNPq) opened a two-year research fellowship call. The selection criterion for both programs was primarily based on the (i) number of publications and (ii) JIF [START_REF] De Meis | Impact factors: just part of a research treadmill[END_REF]. After interviewing some postgraduate students about their concerns in academia, one typical statement was 'The adviser doesn´t care about my thesis so much. He believes that a thesis is the consequence of good work, and good work means papers published in good journals' [START_REF] De Meis | Impact factors: just part of a research treadmill[END_REF].

Chinese policies offering financial reward based on WoS-indexed publications began in earnest in the 1990s, aiming to increase production and international visibility. In some Chinese and Swedish institutions, PhD students should publish at least two articles 'with an average IF' of four to get their degree [START_REF] Quan | Publish or impoverish: An investigation of the monetary reward system of science in China (1999-2016)[END_REF].

In India, recruitment, awards, fellowships and promotions are determined by IF [START_REF] Muthamilarasan | Impact of impact factor in quantifying the quality of scientific research[END_REF].

For the evaluation and ranking of researchers in Ecuador [START_REF]Senescyt establece lineamientos para categorización de investigadores[END_REF], their publications are categorized as follows: (i) "Level 1": publications indexed by WoS or Scopus, Q1 or Q2 in JCR or Scimago Journal Ranking (SJR), (ii) "Level 2": publications indexed by WoS or Scopus, Q3 or Q4 in JCR or SJR, (iii) "Level 3": relevant works and indexed articles not covered by Levels 1 and 2. For faculty hiring [25] peer-reviewed papers count for 2 points per paper, and a maximum of 4 points, and, additionally, indexed papers count for 2 points per paper and a maximum of 10 points. For the overall ranking of universities in Ecuador, similar metrics are used. A group of 74 Ecuadorian academics already criticized this practice [START_REF]El model de evaluacion de las unversidades Ecuatorianas -Apuntes criticos para el debate[END_REF], bringing up the argument (amongst others) that only 242 Latin American journals (out of more than 5000) are indexed in WoS and Scopus, and those typically rank low. Moreover, the currently used metrics result in low ratings for researchers and institutions in the humanities and social science fields.

Scientific community against the way research quality is assessed

The 2012 San Francisco Declaration on Research Assessment (DORA) [START_REF]The San Francisco Declaration on Research Assessment (DORA)[END_REF] was outlined by a group of journal editors and publishers at a meeting of the American Society for Cell Biology (ASCB) and its aim is to promote a world in which the content of a research article is not assessed by the IF of the journal where it appears. Up until now (September 26 th , 2018) the declaration gathered 580 and 12779 online institutional and individual signatures, respectively. Momentum is being built, particularly in the UK, where recently all seven research councils announced their support [START_REF] Curry | Let's move beyond the rhetoric: it's time to change how we judge research[END_REF].

Many authors agree that the IF is not a reliable instrument for measuring the quality of a scientist [START_REF] Hallberg | Can the impact factor measure the quality of research[END_REF][START_REF] Campbell | Escape from the impact factor[END_REF][START_REF] Tregoning | How will you judge me if not by impact factor?[END_REF]. Anthony van Raan, former director of the Centre for Science and Technology Studies at Leiden University (The Netherlands), once said [START_REF] Van Noorden | Metrics: A profusion of measures[END_REF]: 'If there is one thing every bibliometrician agrees, is that you should never use the JIF to evaluate research performance for an article or an individual -that is a mortal sin'. Similar unequivocal opinions can be found from other bibliometricians [START_REF] Glänzel | Springer Handbook of Science and Technology Indicators[END_REF]. A more honest measure of the quality of a paper may be derived from the number of times it is cited [START_REF] Eston | Editorial: The Impact Factor: a misleading and flawed measure of research quality[END_REF][START_REF] Van Diest | Impactitis: new cures for an old disease[END_REF][START_REF] Norris | Citation counts and the Research Assessment Exercise V: Archaeology and the 2001 RAE[END_REF][START_REF] Oppenheim | Do citations count? Citation indexing and the Research Assessment Exercise (RAE)[END_REF].

Randy Schekman, the 2013 Nobel prize winner in medicine, said his lab would no longer send research to the top-tier journals Nature, Cell and Science, which in his opinion are distorting the scientific process and represent a 'tyranny' that must be broken [START_REF] Sample | Nobel winner declares boycott of top science journals[END_REF]. Schekman criticizes those journals for artificially restricting the number of accepted papers, as well as the JIF as a marketing metric used by many prominent journals [START_REF] Sample | Nobel winner declares boycott of top science journals[END_REF]. Besides Schekman, many other Nobel Laureates have spoken out (see Table 1), not directly against top-tier journal's decisions, but against the obsession on publishing in high-impact journals as a consequence of the biased scientific assessment policies taken by governments and institutions. Figures 1234567partially illustrate the interviews given by seven Laureates on that topic.

Novel metrics aiming to make the impact factor more valuable

Current 5-year IF formulae do not account for research published more than five years ago, regardless of how many citations it still receives or how cutting-edge it still remains. Clear examples are masterpieces still prominent today, such as Randall and Sundrum (1999) [START_REF] Randall | Large Mass Hierarchy from a Small Extra Dimension[END_REF] or [START_REF] Li | The Sequence Alignment/Map format and SAMtools[END_REF] [START_REF] Li | The Sequence Alignment/Map format and SAMtools[END_REF], respectively with 10357 (370 in 2018) and 17113 (2747 in 2018) citations until September 26 th , 2018 (source: Google Scholar). In another example [START_REF] Van Diest | Impactitis: new cures for an old disease[END_REF] concerning the Molecular Pathology journal and the Journal of Clinical Pathology, which have a combined JIF, the total number of citations to their papers in the year 2000 was no less than 7144 (making them rank 7 th among all pathology journals for the total number of citations). However, only 930 of those more than 7144 citations were to papers published in 1998-1999, meaning that no more than 13 per cent of citations was used to compute the 2000's JIF. Considering the former, aiming to balance the way research performance is measured, and trying to keep the current Impact Factor definitions useful, a new metric is suggested. The 'Complementary Impact Factor (CIF)' is proposed as the exact complement of the current JIF or 5-year IF. Therefore, it accounts only for citations to articles more than two or five years old, respectively. It is calculated as shown in Eq. ( 2) as the complement for the 2-year JIF and in Eq. (3) as the complement for the 5-year JIF.

2,

# WoS citations in year to papers published in years < ( -2) # papers published in years ( -2)

year n n n CIF n =  (2) 5,
# WoS citations in year to papers published in years < ( -5) # papers published in years ( -5)

year n n n CIF n =  (3)
Figure 2. Some of Joseph Goldstein's answers on 'Is it important to publish in high impact journals?' [START_REF] Media | Impact factors? What counts is the data -Nobel Laureate Joseph Goldstein (YouTube video)[END_REF]56].

As an alternative to CIF and the current IF metrics, the authors would also like to propose a single novel impact factor named 'Timeless Impact Factor (TIF)', where the differences for the current IFs are that it accounts for citations (i) to all publications ever published in the journal, (ii) received until the end of the year preceding the calculation, and (iii) from any source (e.g., WoS, SCOPUS, others) -not just those from WoS-indexed journals (a minute proportion of the citing ones [START_REF] Eston | Editorial: The Impact Factor: a misleading and flawed measure of research quality[END_REF]). Moreover, it is proposed that each citation is weighted as function of its source, as proposed by Abambres and Arab [57]-1.0 for WoS, 0.8 for SCOPUS, and 0.5 for others. The expression of the TIF then reads:

1 1 p i N n ij i j year n p w TIF N = = =  , (4)
where (i) Np is the total number of papers published in the journal before year n, (ii) ni is the number of papers citing paper i before year n, and (iii) wij is the weighted citation from citing article j to cited article i (1.0, 0.8 or 0.5 if the citing article is indexed in WoS, SCOPUS, or other databases, respectively). When the dispersion on citations needs to be studied, the metric using the Gini coefficient as proposed in [START_REF] Cockriel | The influence of dispersion on journal impact measures[END_REF] can be analyzed. As a final remark, the authors suggest the withdrawal of all self-citations (citations from journal articles to the journal in which they are published) for the calculation of any type of impact factor. Not that it is necessarily unethical, but because it helps reducing the extent of 'fabricated IFs' [START_REF] Davis | Impact Factor Denied to 20 Journals For Self-Citation[END_REF]. It is believed that the previously proposed metrics could make the concept of impact factor far more useful, as an average measure of the journal quality.

Final Remarks

This paper highlighted several viewpoints about the widespread misuse of the journal impact factor and indexing databases in the assessment of individual performance of scientists. The authors seriously disagree with this form of evaluation, as already did several Nobel Laureates who publicly spoke out against it. Since the concept inherent to impact factors is not useless, two novel metrics (Complementary and Timeless Impact Factors) are proposed in this work, aiming to contribute to a more sustainable academia.

Author Contributions: Conceptualization and first-draft writing: M.A.; All other contributions: equally distributed among all authors (AS's contribution was given before April 1 st , 2018).

Figure 1 .

 1 Figure 1. Some of Michael Brown's answers on 'What do you think of the emphasis placed on IFs?' [38, 53].

  Abambres M, et al. (2018). Research Counts, Not the Journal, hal-02074859 © 2018 by Abambres et al. (CC BY 4

Figure 3 .

 3 Figure 3. Some of Peter Doherty's answers on 'How important is a journal's impact factor?' [42, 59].

Figure 4 . 8 Figure 5 .

 485 Figure 4. Some of Paul Nurse's answers on 'How can you judge the quality of a researcher?' [45, 61].

Figure 6 .

 6 Figure 6. Some of Bruce Beutler's answers on 'Is it important to publish in the top journals?' [49, 62].

Figure 7 .

 7 Figure 7. Some of Brian Kobilka's answers on 'What do you think of IFs' [51, 52, 63].

Table 1 .

 1 Opinions of Nobel Laureates about the importance placed on JIFs.

Abambres M, et al. (2018). Research Counts, Not the Journal, hal-02074859 © 2018 by Abambres et al. (CC BY 4.0)

Conflicts of Interest:

The authors declare no conflict of interest.