Adrien Quillet
email: adrien.quillet@ls2n.fr

Didier Audrey Queudet
email: audrey.queudet@ls2n.fr

Didier Lime
email: didier.lime@ls2n.fr

Analysis of Polka Contention Manager for use in Multicore Hard Real-Time Systems

Keywords: Computer systems organization → Real-time operating systems; Multicore architectures real-time systems, non-blocking synchronisation, software transactional memory

come   L'archive ouverte pluridisciplinaire

INTRODUCTION AND MOTIVATION

Real-time systems are increasingly used in electronic devices to control physical events. Those systems are designed to satisfy three objectives: (i) logical determinism, so runs with the same inputs always produce the same results, (ii) temporal determinism which guarantees that temporal constraints of every system action will be satisfied, and (iii) reliability which ensures the system is always available.

In the environment in which real-time systems operate, events usually take place concurrently. In order to handle them properly (i.e. to guarantee that all timing constraints will be satisfied), they resort to concurrent programming: each monitored event is managed by a processing entity called task. As multiple tasks can run in parallel over different processor cores, the underlying platform on which the system executes must provide both synchronization and communication mechanisms. In particular, an important aspect is the guarantee of data consistency. Resources shared between several tasks typically have a limit on the number of simultaneous accesses; as a consequence it is possible that a task can not progress due to an unavailable resource. The system must then efficiently manage resources to avoid both deadlocks and starvation while ensuring all the tasks still meet their deadlines.

One common way to protect concurrent modifications to shared memory is to use locks which are well known to be subject to priority inversion and deadlocks. Considering multicore platforms, another issue inherent to the use of such blocking mechanisms is that parallelism can be severely impacted since concurrent tasks competing for the same lock can be blocked, thus reintroducing some sequential execution in the parallel application. Recently [START_REF] Jiang | On the Analysis of Parallel Real-Time Tasks with Spin Locks[END_REF], spin locks were studied for parallel real-time tasks in where each parallel task is scheduled exclusively on several pre-assigned processors (i.e., by the federated scheduling approach). This reduces the need for locks or scheduling to synchronize concurrent access (through shared resources may introduce locking as considered by Dinh et al. [START_REF] Dinh | Blocking analysis for spin locks in real-time parallel tasks[END_REF]). The authors developed new schedulability analysis techniques for parallel tasks with spin locks, and analysed blocking times but the analysis is pessimistic.

Another way to manage shared resources is to use the concept of transactional memory [START_REF] Herlihy | Transactional memory: Architectural support for lock-free data structures[END_REF], which aims to significantly ease development and maintenance of concurrent programs. Transactional memory implementations exist both in hardware (HTM -Hardware Transactional Memory), in software (STM -Software Transactional Memory), or under schemes that combine both hardware and software (Hybrid TM -Hybrid Transactional Memory). In HTM systems, transactional memory support is implemented by modifying the data-cache protocols to support version management and conflict detection. The close synergy of the hardware with the processor core and cache allow these systems to provide very high levels of performance. Nevertheless, this type of TM system is usually bound by some sort of capacity contraints, e.g. the hardware can handle a specific fixed read-/write-set size. In contrast, STMs allow to build very flexible prototypes, as the full concurrency control is implemented in software. In return, STMs have a reputation for being slower than HTMs. However, considering the conceptual benefits of STMs, we will focus only on STMs in this paper. They allow programmers to embed a sequence of operations applied to shared resources into a transaction. Every transaction accesses shared data in memory without interfering with other transactions, and appears to them as executed atomically. To deal with inconsistencies, transactional memories usually use contention managers (CM) to resolve conflicts between transactions. Contention managers allow some transactions to commit (i.e. the data modifications are then made permanent), and force other conflicting ones to abort (i.e. all the modifications are discarded and the transaction restarts from the beginning), based on their internal policy.

Because software transactional memories hide to developers the way atomicity is obtained, it is essential to prove the correctness of their mechanisms, especially when used in realtime systems. In this paper, we introduce new assumptions on the execution time of transactions. We formally prove that the use of the lock-free contention manager Polka [START_REF] Scherer | Advanced contention management for dynamic software transactional memory[END_REF] in such constrained systems is sufficient to guarantee that every transaction progresses, bringing in upper bounds on the execution time and the number of abortions of a transaction.

The rest of this paper is organized as follows. We first present related works about transactional memories in Section 2. We then recall the main concepts of STM in Section 3. Section 4 introduces the formalization of the system we study. Section 5 focuses on Polka contention manager and contains formal proofs about its progress property. Finally, Section 6 concludes the paper.

RELATED WORK 2.1 Transactional Memory

Herlihy et al. were the first to propose a hardware based transactional synchronization methodology [START_REF] Herlihy | Transactional memory: Architectural support for lock-free data structures[END_REF] that uses the cache coherence protocol to detect conflicts. Since then, the research community has produced many different HTMs [START_REF] Dice | Early experience with a commercial hardware transactional memory implementation[END_REF][START_REF] Harris | Transactional memory[END_REF][START_REF] Herlihy | Obstruction-free synchronization: Double-ended queues as an example[END_REF][START_REF] Jacobi | Transactional memory architecture and implementation for IBM system Z[END_REF] that are more efficient. Chip vendors have increasingly begun to integrate HTM in their processors like the AMD's Advanced Synchronization Facility (ASF) [START_REF] Hung | ASF: AMD64 Extension for Lock-Free Data Structures and Transactional Memory[END_REF]. Transactional synchronization extensions (TSX) whose performance was recently analysed in [START_REF] Kangmin | ParaTM: Transparent Embedding of Hardware Transactional Memory for Traditional Applications[END_REF] were also adopted by Intel for its processors in the year 2012. However, since HTMs require hardware facilities, they are not suitable for most of multicore processors. Other software-based implementations using common atomic instructions such as CAS (Compareand-Swap) or LL/SC (Load Linked/Store Conditional) [START_REF] Jensen | A new approach to exclusive data access in shared memory multiprocessors[END_REF], were first proposed by Shavit and Touitou in [START_REF] Shavit | Software transactional memory[END_REF]. By nature, they are less efficient than HTM but they can be used with all multicore processors.

TM Correctness and Timing Analysis

The first steps to formally verify TM systems were made through Greedy [START_REF] Guerraoui | Toward a theory of transactional contention managers[END_REF] and FTGreedy [START_REF] Guerraoui | Robust contention management in software transactional memory[END_REF] CM proposals. Guerraoui et al. proposed a new and robust CM that provides provable properties (e.g. every transaction commits within bounded time). They also introduced the notion of opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF], a correctness criterion for TM implementations.This idea was extended by Imbs et al. in [START_REF] Imbs | On the consistency conditions of transactional memories[END_REF]. Schoeberl et al. proposed Real-Time Transaction Memory (RTTM) [START_REF] Schoeberl | RTTM: Realtime transactional memory[END_REF], a new hardware-implemented synchronization paradigm for hard real-time systems. Their demonstrate that, provided the transaction conflict resolve time is bounded, tasks will meet their deadlines. Nevertheless, they do not provide any guarantees that transactions will complete successfully.

Sarni et al. presented Real-Time STM [START_REF] Sarni | Realtime support for software transactional memory[END_REF], a TM protocol ensuring lock-freedom, a weaker property than wait-freedom, that does not guarantee that all transactions will meet their deadlines, thus being suitable only for soft real-time systems.

Upper bounds for the number of transaction retries in a real-time system were provided by Schoeberl et al. [START_REF] Schoeberl | RTTM: Realtime transactional memory[END_REF] and El-Shambakey et al. [START_REF] El-Shambakey | STM concurrency control for embedded real-time software with tighter time bounds[END_REF][START_REF] El-Shambakey | On real-time STM concurrency control for embedded software with improved schedulability[END_REF]. However, the conditions were very simple, with periodic tasks and one transaction performed by each task.

Cotard et al. [START_REF] Cotard | STM-HRT: A Robust and Wait-Free STM for Hard Real-Time Multicore Embedded Systems[END_REF] proposed a new STM for hard real-time systems, that relies on a wait-free protocol that enforces progress of every task and that can be integrated in the WCET of tasks during the timing analysis of the system. However, the approach is restricted to transactions that manipulate objects in a single access mode, either read or write.

Barros et al. [START_REF] Barros | Response time analysis of hard real-time tasks sharing software transactional memory data under fully partitioned scheduling[END_REF] addressed the response time analysis of hard real-time tasks, which share STM data under partitioned scheduling strategies. They assume that transactions are serialised according to their arrival time and they are managed by following a FIFO contention manager for real-time systems (FIFO-CRT) [START_REF] Barros | Non-preemptive scheduling of real-time software transactional memory[END_REF].

Although those works are close in purpose to ours, none of them prove the wait-freedom property (i.e. all trans-actions progress) among existing CMs.

BACKGROUND MATERIAL 3.1 Software Transactional Memory Concepts

A transaction, as originally formalized in [START_REF] Kapali | The notions of consistency and predicate locks in a database system[END_REF], is based on the notion of synchronization point, which represents a durable and consistent state of a computer system. This notion relies on the four ACID properties [START_REF] Haerder | Principles of transactionoriented database recovery[END_REF]:

• Atomicity. The sequence of operations either all occur (the transaction commits), or nothing occur (the transaction aborts), which makes the sequence of operations indivisible. • Consistency. The transaction starts and ends in a valid system state. • Isolation. A transaction being executed is unaware of other executing transactions. • Durability. Once a transaction has been committed, it will remain so.

During its execution, a transaction will manipulate one or several data, either in reading or writing modes. This set of data is called the transaction dataset. Definition 3.1. Two transactions are said in contention if they both access a same resource during their execution and one of them may update it. Definition 3.2. Two transactions are said in conflict if they performed an operation on the same resource and one of them updated it.

An STM needs a data version management policy in order to maintain old values, needed to abort the transaction, and new values, needed to commit the transaction. Concurrency control is based on a conflict detection policy which defines the rules triggering the abortion of a transaction. There are two approaches: (i) with the eager approach, conflicts are detected and resolved as soon as they occur, (ii) with the lazy approach, conflicts detection and resolution occur later, generally before trying to commit the transaction. Finally, a transactional memory typically has a contention manager module [START_REF] Herlihy | Software transactional memory for dynamicsized data structures[END_REF], which is in charge of resolving conflicts between transactions. Depending on its contention policy (see [START_REF] Scherer | Advanced contention management for dynamic software transactional memory[END_REF] for a survey), the CM decides which of the conflicting transactions can continue, and as a result, which transaction(s) must abort.

Polka Contention Manager

The Polka contention manager [START_REF] Scherer | Advanced contention management for dynamic software transactional memory[END_REF] favors the transactions which performed the greater number of operations. The chosen criterion to quantify how much work has been done at a given time is the number of data already accessed either in reading or writing mode; it is called karma and is denoted by 𝑘. It is a component of the state of the transaction. Transactions start with a zero karma which is incremented by one at each first access to a data (first access is renewed each time the transaction starts or restarts its operations) or at each abortion of the transaction. When a transaction aborts, the maximum number of times it may restart is bounded by the difference in karma between itself and its enemy. Moreover, Polka introduces an exponential backoff between successive transaction restarts. Every aborted transaction waits for a random duration that increases exponentially. When a transaction commits, its karma returns to zero.

MODELS AND TERMINOLOGY 4.1 System Model

We consider a platform made of 𝑚 identical processor cores 𝜋 = {𝜋 1 , . . . , 𝜋𝑚}, so the maximum number of task instances that can run in parallel is 𝑚.

Time Representation.

The system time sequence 𝑡 = 𝑡 𝑖1≤𝑖 is a sequence of countable instants. We denote by T the domain of 𝑡. At any time, the difference between two subsequent instants 𝑡 𝑖+1 and 𝑡 𝑖 is 1; this minimum period is called a time unit. We assume that every shared resource managed by an STM is actually manipulated with an object. We denote by 𝑂 𝒮 the finite set of system objects such that 𝑂 𝒮 = 𝑂 Σ ∪ 𝑂 Σ , where 𝑂 Σ and 𝑂 Σ denote the finite set of objects used only outside (resp. inside) an explicit transaction. The final set of all possible values for system objects is denoted by ϒ ⊥ = ϒ ∪ {⊥} where ϒ represents the finite set of all possible defined values for the objects whereas ⊥ stands for the undefined value. The value of objects is given by a function Val 𝒮 : 𝑂 𝒮 → ϒ ⊥ such that:

Val 𝒮 𝑜 = 𝑥 iff x is the value of object o 4.1.3 Operations.
Let Θ 𝒮 denote the finite set of system operations. We consider three possible operations:

• read𝑜: ∀𝑜 ∈ 𝑂 𝒮 , it returns the value of object 𝑜 (i.e. Val 𝒮 𝑜); • write𝑜, 𝑥: ∀𝑜 ∈ 𝑂 𝒮 , 𝑥 ∈ ϒ ⊥ , it writes the value 𝑥 in object 𝑜; • nop: it stands for the idempotent operation, thus leaving the system in the same state as it was before.

We assume that each operation requires one time unit to be performed. Note that every other kind of operations (e.g. arithmetic ones) can be abstracted to a sequence of read(), write() and nop() operations. In order to model an operation that takes more than one time unit to execute, the operation has to be preceded by nop() operations. As a result, to model an operation that requires 𝑘 time units, it must be preceded by 𝑘 -1 idempotent operations, as illustrated in Figure 1.

Task Model

Let 𝑇 𝒮 denote the finite set of system tasks. A task 𝜏 𝑖 is a tuple ⟨𝜋 𝑖 , 𝜑 𝑖 , 𝑇 𝑖 , Σ 𝑖 ⟩, where 𝜋 𝑖 is the processor core on which all instances (or jobs) of 𝜏 𝑖 will be executed, 𝜑 𝑖 is the offset of first activation of the task, 𝑇 𝑖 is the minimum period between two activations of the task and Σ 𝑖 is the finite set of transactions launched during every job.

Each system task 𝜏 𝑖 produces an infinite number of successive jobs J 𝑖,𝑗 , with 𝑗 ∈ N * , as illustrated in Figure 2. All jobs of a given task are assumed independent. Job J 𝑖,𝑗 corresponds to the 𝑗 th activation of task 𝜏 𝑖 . We denote by 𝑟 𝑖,𝑗 ≥ 𝑟 𝑖,𝑗-1 + 𝑇 𝑖 the release time of job J 𝑖,𝑗 . The release time 𝑟 𝑖,0 of the first job of task 𝜏 𝑖 is equal to 𝜑 𝑖 . Definition 4.1. A job is said active as soon as released. At any time, there exists at most one active job for a given task. An active job can be preempted at some time 𝑡𝑛, except if it is executing a transaction.

𝜋 𝑡 1 𝑡 𝜋 𝑖 J𝑖,1 J𝑖,2 J𝑖,3 𝜑 𝑖 𝑇 𝑖 𝑇 𝑖 𝑇 𝑖 𝑟𝑖,1 𝑟𝑖,2 𝑟𝑖,3 𝑟𝑖,4

Transaction Model

First, we assume that a transaction only belongs to one task.

Formalization. A transaction

𝜎 𝑖 is a tuple ⟨𝑏 𝑖 , 𝑁 𝑖 , Ω 𝑖 , 𝑂 𝑖 ⟩,
where 𝑏 𝑖 represents its start time, 𝑁 𝑖 is the number of operations in the transaction, Ω 𝑖 is its dataset with Ω 𝑖 ⊆ 𝑂 Σ and 𝑂 𝑖 is the transaction private memory, which contains copies of the objects used by the transaction. This private memory is only visible to the transaction itself. Hence, a transaction works on its own copies of the objects and if it successfully commits, then the commit phase is completed by copying the private modifications into the shared memory.

We denote by 𝜂 𝑖 = ⟨𝜉 𝑖 , 𝑛 𝑖 , 𝜔 𝑖 , 𝑐 𝑖 , Val 𝑖 ⟩ the state of 𝜎 𝑖 , where 𝜉 𝑖 is the current status of 𝜎 𝑖 , 𝑛 𝑖 is the actual number of performed operations, 𝜔 𝑖 is its finite set of already opened objects with 𝜔 𝑖 ⊆ Ω 𝑖 , 𝑐 𝑖 is its internal clock starting at 0 and increased by one at each performed operation, and Val 𝑖 from 𝑂 𝑖 → ϒ ⊥ , is the function giving the value of an object from its transaction private memory. There exists 5 different transaction status:

• NotStarted is the status of a transaction that has never started; • Running is the status of a processing transaction which has at least one more operation to perform; • Checking is the status of a transaction which performed all its operations, and is verifying that its modifications will not leave the system in an inconsistent state; • Aborted is the status of a transaction which has been aborted; • Committed is the status of a transaction that has completed its execution. All committed modifications are visible to the entire system. We denote by Exec Σ 𝑡𝑛 the set of processing transactions at time 𝑡𝑛, and by Active Σ 𝑡𝑛 the set of active transaction the same time.

We denote by Σ the finite set of system transactions and by 𝒩 = {𝜂 1 , . . . , 𝜂 |Σ| } the finite set of transaction states.

Let Θ Σ denote the finite set of operations specific to transactions, such that it exists 5 different operations related to transactions:

• start: starts transaction 𝜎 𝑖 , initializing all its parameters properly. • restart: restarts transaction 𝜎 𝑖 after an abortion. This operation resets all transaction parameters except its start time which remains unchanged.

• check: brings transaction 𝜎 𝑖 into checking phase. This operation checks if all previously opened objects keep the same values, thus detecting potential conflicts with other transactions. • abort: cancels all modifications made inside the transaction itself. • commit: makes all modifications made by the transaction visible for the entire system.

Note that depending on other currently executed transactions and on the read-/write-set sizes, the execution time of check, abort, and commit operations may vary.

Transactions can also perform any operation of Θ 𝒮 . Accordingly, the domain of arguments of system operations is extended to 𝑂 𝒮 ∪ 𝑂 1 ∪ . . . 𝑂 |Σ| . The set of operations that is possible to perform from a given status is illustrated in Figure 3.

Properties.

The system state resulting of the parallel execution of transactions is consistent only if this execution is serializable. Definition 4.4. A parallel execution of 𝑛 transactions is serializable if it is equivalent to a serial execution of these 𝑛 transactions.

We propose to distinguish the following notion of transaction correctness.

Let TT (Turnaround Time) denote the upper bound on the time during which transactions can remain active in the system. This bound is set a priori by programmers. For instance, considering a real-time application, this upper bound may be set according to the real-time constraints of the tasks, using a worst case execution time (WCET) analysis. Definition 4.5. A transaction is said timely correct if the maximum period between its (start()|restart()) and (abort() | commit()) operations is less than or equal to TT. Otherwise (i.e. this period is exceeded), the transaction is said timely incorrect.

Since a transaction has to perform at least one system operation other than nop() and three specific operations (start(), check() and commit()) to be valid, the minimum value of TT is 4 time units.

Let 𝜎 𝑖 † 𝜎 𝑗 (resp. 𝜎 𝑖 ‡ 𝜎 𝑗 ) denote the fact that transactions 𝜎 𝑖 and 𝜎 𝑗 are in contention (resp. in conflict). By extension, we denote by 𝜎 𝑖 † Enemies 𝑖 (resp. 𝜎 𝑖 ‡ Enemies 𝑖 ) the fact that 𝜎 𝑖 is in contention (resp. in conflict) with every transaction of the transaction set Enemies 𝑖 . For ease of reference, notations previously presented are summarized in Table 1.

SCOPING POLKA CM

In this section, we discuss how the karma values assigned by Polka CM to transactions may vary along time. In particular, we study the extreme cases for which transactions exhibit minimal or maximal karma values.

Let us first recall how conflicts are resolved in Polka CM. So, let us assume that at a given time there exists both a checking transaction 𝜎 𝑖 and a set Enemies 𝑖 of transactions conflicting with 𝜎 𝑖 . The following two cases are therefore possible:

• ∀𝜎𝑒 ∈ Enemies 𝑖 : 𝑘 𝑖 > 𝑘𝑒: every enemy transaction aborts and 𝜎 𝑖 commits, Considering lazy conflict detection (check() operation occurs right before commit() operation), we can deduce the two following commit rules:

• If the writer commits, then all readers whose read() operation is performed abort; • If a reader commits, then all readers commit and the writer aborts if its write() operation is already performed.

Let's investigate Polka arbitration among competing transactions. All transactions earn one karma unit for their execution, and one more karma unit if they abort. At the beginning of the execution, all karmas are equal to zero; the writer will commit first because it runs faster than readers. Its karma will then return to zero while the karma of all readers will be of 2 (one for the performed operation, and one for the abortion). The writer is a priori favored since it reaches validation before any reader, but Polka contention manager favors transactions that have opened the greater number of objects, their karma being incremented by one at each first object opening. As a result, if the writer's karma is lower than the karma of readers, the writer will sleep, waiting for readers to commit (see Figure 4). The only chance for readers to validate is if the writer total sleeping period is strictly greater than the difference of karma between readers and writer. If so, readers commit successfully while the writer still sleeps; the writer is aborted, its karma is increased by one and the karma of all readers return to zero.

The sleeping period being randomly drawn from an interval growing exponentially, the more readers are aborted, the more likely they are to validate, because the writer sleeping period has a chance to exponentially grow.

Without studying more specifically Polka policy, we cannot say if readers will eventually validate. They have more and more chances to commit, but if the total sleeping period of the writer indefinitely remains lower than the difference of karma between the readers and the writer, then the writer will indefinitely abort all readers. Hereafter, we focus on the worst (i.e. slowest) and best (i.e. fastest) karma accumulation for transactions in terms of speed.

Slowest Karma Accumulation

Lemma 5.1. In a system using a software transactional memory whose contention manager is Polka, the slowest karma accumulation at time 𝑡𝑛 of a timely correct transaction 𝜎 𝑙 is given by:

𝑘 𝑙 = ⌊ 𝑡𝑛 -𝑏 𝑙 TT ⌋ × 2 + 𝜖 𝑙 with 𝜖 𝑙 ∈ {0, 1}
Proof. Let 𝜎 𝑙 denote the timely correct transaction whose karma increases the slowest. According to Polka policy, the slowest way to increase karma is to manipulate the fewest possible objects, while taking the maximum amount of time to do it. Since we study karma accumulation, it is assumed that this transaction indefinitely aborts. Hence 𝜎 𝑙 must have a single operation to perform (so its dataset contains only one object). The timing diagram for the execution of 𝜎 𝑙 is illustrated in Figure 5. Transaction 𝜎 𝑙 increases its karma by one not only when it accesses its single object but also at each abort() operation. As a result, its karma is increased by 2 every TT time units. So, at given time, the karma of 𝜎 𝑙 is double the number of execution cycles of the transaction, in addition to the karma 𝜖 𝑙 accumulated during the current execution cycle. □

Fastest Karma Accumulation

Lemma 5.2. In a system using a software transactional memory whose contention manager is Polka, whose conflict detection is lazy and in which all transactions are timely correct, the fastest karma accumulation at time 𝑡𝑛 of transaction 𝜎𝑤 is given by:

𝑘𝑤 = ⌊ 𝑡𝑛 -𝑏𝑤 TT ⌋ × ( TT -2 ) + 𝜖𝑤 with 𝜖𝑤 ∈ {0, . . . , 𝑛}
Proof. Let 𝜎𝑤 denote the timely correct transaction whose karma increases the fastest. According to Polka policy, the fastest way to accumulate karma is to access as many various objects as possible in a minimum amount of time. Because (start()|restart()) and check() operations do not increase karma, a timely correct transaction accessing as many objects as possible in TT time units eventually has a greater karma than a transaction accessing a single object in one time unit that is aborted and restarted over a period of TT time units. As previously, it is also assumed that this transaction indefinitely aborts.

Transaction 𝜎𝑤 thus accesses to a maximum number of objects over its interval of correctness, keeping the remaining time units to perform operations (start()|restart()), check() and (abort()). The timing diagram for the execution of 𝜎𝑤 is illustrated in Figure 6.

Transaction 𝜎𝑤 increases its karma by one for each performed operation or abort() operation. Consequently, its karma is increased by

( TT -2
) every TT time units. So, at a given time, the karma of 𝜎𝑤 is

( TT -2 )
times the number of execution cycles of the transaction, in addition to the karma 𝜖𝑤 accumulated during the current execution cycle. □

Achieving the Greatest Karma

Lemma 5.3. In a system using a software transactional memory whose contention manager is Polka, whose conflict detection is lazy and in which all transactions are timely correct, the maximum possible karma value is

𝑘 max 𝒮 = ( min ( |𝜋|, |Σ| ) -1 ) × ( TT -2 ) + 𝜖 with 𝜖 ∈ {0, . . . , 𝑛}
Proof. Let us argue by contradiction, assuming that there is no upper bound on the karma.

First, let us study the trivial case where there is only one transaction in the system. A single transaction cannot be in conflict with itself and thus cannot be aborted. As a consequence, this single transaction always commits and always achieves the greatest karma which is the number of objects it accessed. Hence there exists an upper bound 𝜖 on the karma equals to the number of objects opened by the transaction during its execution.

Let now consider that there are at least two timely correct transactions 𝜎𝑤 and 𝜎 𝑤 ′ in the system, such that there is no upper bound on their karma. Assuming that 𝑘 𝑖 𝑡𝑧 denote the karma of a transaction 𝜎 𝑖 at time 𝑡𝑧, this can be expressed by the following property:

∀𝑡𝑛, ∃𝑡𝑚 > 𝑡𝑛 : ( 𝑘𝑤𝑡𝑛 < 𝑘𝑤𝑡𝑚 ) ∨ ( 𝑘 𝑤 ′ 𝑡𝑛 < 𝑘 𝑤 ′ 𝑡𝑚 ) (1)
Let us prove this property is false.

The lack of upper bound on the karma means that there is no upper bound on the number of abortions of a transaction. As a consequence, there always exists a transaction which karma is greater than the previous greatest karma value. Note that the transaction with the greatest karma can vary over time. To examine the evolution of karma, we consider the worst-case execution for system transactions. We assume that all transactions accumulate karma the fastest way and share the same dataset; the timing diagram of their execution is illustrated in Figure 6. To maximize contention between transactions, we also consider the execution case illustrated in Figure 7. The maximum number of concurrent transactions is the minimum between the number of system transactions and processor cores, and all transactions start at the same time.

Let 𝜎𝑤 denote the transaction executed on processor core 𝜋𝑤. Transaction 𝜎𝑤 reaches its checking phase before any All transactions start at the same time and are based on the same model (as illustrated in Figure 6). As a result, if a transaction commits, it forces the abortion of all other transactions.

other transaction; all transactions having the same karma, 𝜎𝑤 has to sleep, waiting for other transactions to commit or abort. According to the execution case, all transactions are in conflict, so only one transaction will be allowed to commit. The last transaction reaching its checking phase will commit, and other transactions will abort, particularly 𝜎𝑤. After a bounded number of abortions and always according to the execution pattern illustrated in Figure 7, 𝜎𝑤 will possess the greatest karma in the system. Let 𝜎 𝑤 ′ denote the transaction that possesses the second greatest karma in the system; it is the transaction that committed first in the system. According to Lemma 5.2, at time 𝑡𝑛, the karma of 𝜎 𝑤 ′ can be expressed as:

𝑘 𝑤 ′ = ⌊ 𝑡𝑛 -𝑏 𝑤 ′ TT ⌋ × ( TT -2 ) + 𝜖 𝑤 ′ with 𝜖 𝑤 ′ ∈ {0, . . . , 𝑛}
while the karma of 𝜎𝑤 is:

𝑘𝑤 = ⌊ 𝑡𝑛 -𝑏𝑤 TT ⌋ × ( TT -2 ) + 𝜖𝑤 with 𝜖𝑤 ∈ {0, . . . , 𝑛}
Since 𝜎𝑤 has executed one more execution cycle than 𝜎 𝑤 ′ , and considering they have the same execution pattern, the karma of 𝜎𝑤 can also be expressed as:

𝑘𝑤 = ⌊ 𝑡𝑛 -𝑏 𝑤 ′ -TT TT ⌋ × ( TT -2 ) + 𝜖 𝑤 ′ = ( ⌊ 𝑡𝑛 -𝑏𝑤 TT ⌋ + 1 ) × ( TT -2 ) + 𝜖𝑤
As a result, the maximal difference of karma between 𝜎𝑤 and

𝜎 𝑤 ′ is ( TT -2
)

. We then distinguish two possible cases:

• case (i): 𝜎 𝑤 ′ tries to commit first.

• case (ii): 𝜎𝑤 tries to commit first.

case (i):

If 𝜎 𝑤 ′ tries to commit first, then 𝜎 𝑤 ′ will sleep, waiting for 𝜎𝑤, because the karma of 𝜎𝑤 is greater than its karma. The difference of karma between 𝜎𝑤 and 𝜎 𝑤 ′ being

( TT -2 ) , 𝜎 𝑤 ′ will sleep at least ( TT -2
) time units before aborting 𝜎𝑤. Transaction 𝜎𝑤 being in checking phase too, and considering its execution pattern, 𝜎 𝑤 ′ only has one time unit to abort 𝜎𝑤 to commit, i.e. TT-2 ≤ 1, that is equivalent to TT ≤ 3. By definition, TT ≥ 4. As a consequence, 𝜎 𝑤 ′ cannot commit before 𝜎𝑤.

case (ii): If 𝜎𝑤 tries to commit first, then 𝜎𝑤 will commit because it has the greatest karma.

In both cases, the karma of 𝜎𝑤 at 𝑡𝑛 allows it to commit. If 𝜎𝑤 can commit, its karma cannot indefinitely increase. We can deduce the same fact for other transactions since they all share the same execution pattern. As a consequence, there exists an upper bound on the karma. According to the execution pattern of transactions, the greatest karma is equal to the number of concurrent transactions (not counting the current transaction) times the karma accumulated during an execution cycle (i.e.

(

TT -2 )
) in addition to the karma accumulated during its last cycle (at most 𝑛). This contradicts Property 1. □ Lemma 5.4. In a system using a software transactional memory whose contention manager is Polka, whose conflict detection is lazy and in which all transactions are timely correct, the maximum period needed by a recurring aborted transaction 𝜎 𝑙 to reach the maximum possible karma 𝑘 max 𝒮 is given by:

∆ max 𝑙 = ( ⌊ 𝑘 max 𝒮 2 ⌋ + 1
)

× TT

Proof. According to Lemma 5.1, the slowest karma accumulation is 2 karma units every TT time units for a timely correct transaction that always aborts. According to Lemma 5.3, there exists an upper bound 𝑘 max 𝒮 on the karma that is possible to accumulate in the system. As a consequence, there exists an upper bound on the time needed to reach this karma limit.

Assuming the worst-case execution, a timely correct transaction increases its karma by 2 every TT time units. As a consequence, after ⌊ 𝑘 max 𝒮 2 ⌋ cycles of execution, the karma of this transaction is near or equal to 𝑘 max 𝒮 . Obviously, if it has not already happened, the transaction will reach the karma limit during its next cycle of execution. We obtain the upper bound established in the Lemma. □ 5.5 Polka: a Wait-free CM Theorem 5.5. In a system using a software transactional memory, which contention manager is Polka, and which conflict detection is lazy, if every transaction is timely correct, then every transaction progresses.

Proof. We assume that in such a system, there exists a timely correct transaction 𝜎 𝑙 that never progresses, as expressed by the property:

∃𝑡 𝑖 : 𝜎 𝑙 ∈ Actives𝑡 𝑖 ∧ ∀𝑡 𝑗 > 𝑡 𝑖 : 𝜉 𝑙 Committed (2)
Let us prove this property is false. Let Enemies 𝑙 𝑡𝑚 denote the set of transactions in conflict with 𝜎 𝑙 at time 𝑡𝑚. We need to study four different cases:

• 𝜉 𝑙 = Checking ∧ 𝜎 𝑙 ‡ Enemies 𝑙 (i.a) ∀𝜎𝑒 ∈ Enemies 𝑙 : 𝑘 𝑙 > 𝑘𝑒 (i.b) ∃𝜎𝑒 ∈ Enemies 𝑙 : 𝑘 𝑙 ≤ 𝑘𝑒 • 𝜉 𝑙 = Running ∧ 𝜎 𝑙 ‡ Enemies 𝑙 (ii.c) ∃𝜎𝑒 ∈ Enemies 𝑙 : 𝜉𝑒 = Checking ∧ 𝑘𝑒 > 𝑘 𝑙 (ii.d) ∃𝜎𝑒 ∈ Enemies 𝑙 : 𝜉𝑒 = Checking ∧ 𝑘𝑒 ≤ 𝑘 𝑙 (i.a).
Transaction 𝜎 𝑙 is in checking phase and its karma is strictly greater than the karma of every transaction conflicting with it. Transaction 𝜎 𝑙 is allowed to commit, and all conflicting transactions are aborted. It contradicts Property 2.

(i.b).

Transaction 𝜎 𝑙 is in checking phase and there is at least one transaction 𝜎𝑒 ∈ Enemies 𝑙 having a karma greater or equal to 𝜎 𝑙 's one. Transaction 𝜎 𝑙 sleeps, waiting for 𝜎𝑒. As a result, there are four possible cases:

(1) Transaction 𝜎𝑒 commits.

(ii.c).

There is at least one checking transaction 𝜎𝑒 in conflict with 𝜎 𝑙 having a karma strictly greater than 𝜎 𝑙 's one. Transaction 𝜎 𝑙 aborts and 𝜎𝑒 commits (see Figure 8). According to Lemma 5.4, there exists a time 𝑡𝑛 > 𝑡𝑚 such that 𝜎 𝑙 reaches the karma limit, i.e. ∀𝜎𝑒 ∈ Enemies 𝑙 𝑡𝑛 : 𝑘 𝑙 > 𝑘𝑒. We refer to cases i.a and ii.d.

(ii.d).

There is at least one checking transaction 𝜎𝑒 in conflict with 𝜎 𝑙 having a karma lower or equal to 𝜎 's one. 𝜎𝑒 sleeps, waiting for 𝜎 𝑙 . As a result, there are four possible cases:

(1) Transaction 𝜎 𝑙 commits. Transaction 𝜎𝑒 aborts (see Figure 8). It contradicts Property 2. (2) Transaction 𝜎 𝑙 aborts. Transaction 𝜎𝑒 is allowed to commit if it is not aborted too. We refer to case ii.d.4. (3) 𝑤 𝑒,𝑙 < 𝑤 𝑚𝑎𝑥 𝑒,𝑙 , the number of sleeping periods is not greater than the difference between 𝜎𝑒 and 𝜎 𝑙 karmas. Transaction 𝜎𝑒 sleeps again, waiting for 𝜎 𝑙 (see Figure 9). We refer to cases ii.d.1, ii.d.2 and ii.d.4. (4) 𝑤 𝑒,𝑙 = 𝑤 𝑚𝑎𝑥 𝑒,𝑙 , the maximum number of sleeping periods is reached. Transaction 𝜎 𝑙 aborts and transaction 𝜎𝑒 commits (see Figure 9). Let investigate this last case. By hypothesis, 𝜎 𝑙 never progresses, that is in this precise situation, transaction 𝜎𝑒 always aborts 𝜎 𝑙 by reaching the maximum number of sleeping periods. Without loss of generality, we assume the virtual worst-case execution for 𝜎 𝑙 : this transaction accumulates karma the slowest way, as described by Lemma 5.1. Transaction 𝜎𝑒 accumulates karma the fastest way, as described by Lemma 5.2. Since both transactions are timely correct, their execution time, including sleeping periods, cannot be greater than TT. As a consequence, the maximum number of sleeping periods is TT. This is expressed by the following inequality:

𝑘 𝑙 -𝑘𝑒 ≤ TT (3)
with

𝑘 𝑙 = ⌊ 𝑡𝑛 -𝑏 𝑙 TT ⌋ × 2 + 𝜖 𝑙 𝑘𝑒 = ⌊ 𝑡𝑛 -𝑏𝑒 TT ⌋ × ( TT -2 ) + 𝜖𝑒
Since 𝜎𝑒 already aborted 𝜎 𝑙 at least one time, it started right after 𝜎 𝑙 , considering the worst-case execution. So 𝜎𝑒 karma can be expressed as:

𝑘𝑒 = ⌊ 𝑡𝑛 -𝑏 𝑙 + 1 TT ⌋ × ( TT -2 ) + 𝜖𝑒 = ⌊ 𝑡𝑛 -𝑏 𝑙 TT ⌋ × ( TT -2 ) + 𝐶𝑒
with 𝐶𝑒 being a constant value which is equal to the sum of all constants in the previous inequality. The inequality 3 can be rewritten as:

( ⌊ 𝑡𝑛 -𝑏 𝑙 TT ⌋ × 2 + 𝜖 𝑙 ) - ( ⌊ 𝑡𝑛 -𝑏 𝑙 TT ⌋ × ( TT -2 ) + 𝐶𝑒 ) ≤ TT 𝑡𝑛 -𝑏 𝑙 + 𝜖 𝑙 -𝐶𝑒 ≤ TT 𝑡𝑛 ≤ TT + 𝑏 𝑙 -𝜖 𝑙 + 𝐶𝑒 𝑡𝑛 ≤ 𝐶
with 𝐶 being a constant value which is equal to the sum of all constants in the inequality. The system time sequence 𝑡 being a strictly increasing sequence without supremum, the inequality 3 is incorrect. As a consequence, there is no transaction 𝜎𝑒 such that 𝜎𝑒 always aborts 𝜎 𝑙 . It contradicts the Property 2.

□

CONCLUSION AND FUTURE WORK

While software transactional memory performances are widely studied, the question of the correctness of such mechanisms remains open. The few papers that investigated this issue actually focused on the design of new contention managers and on the modeling of transactions themselves, while there exists STM implementations with empirically efficient CMs. Motivated by this observation, we introduced new assumptions on the execution time of transactions into real-time systems in order to formally prove that, provided these systems use the existing Polka CM, they can ensure the progress of all transactions. Based on an fine-grain modeling of the whole system, we also derived upper bounds on both the execution time and the number of abortions of transactions. Future work include the proposal of a robust variant of Polka CM, by introducing static priorities that would allow to relax the functional and timing constraints of transactions. Indeed, in the case where a transaction becomes timely incorrect, there is actually no guarantee that all timely correct transactions will progress. 𝜎 𝑙 is necessarily timely correct: 𝜎 𝑒 will ultimately abort 𝜎 𝑙 when reaching the maximum number of sleeping periods.

Figure 1 :

 1 Figure 1: Execution model for a 4 time units operation

Figure 2 :

 2 Figure 2: Execution of a task 𝜏 𝑖 = ⟨𝜋 𝑖 , 𝜑 𝑖 , 𝑇 𝑖 , Σ 𝑖 ⟩

Definition 4 . 6 .

 46 The sequence of operations performed between (start()|restart()) and (abort()|commit()) operations (included) of a transaction is called cycle of execution of this transaction. Definition 4.7. A transaction 𝜎 𝑖 progresses if, at a given time 𝑡𝑛, 𝜎 𝑖 ∈ Active Σ 𝑡𝑛 and there exists 𝑡𝑚 > 𝑡𝑛 such as at time 𝑡𝑚, the status of 𝜎 𝑖 is Committed.

Figure 4 :

 4 Figure 4: Fast single-writer/Slow multiple-reader scenario

Figure 5 :

 5 Figure 5: Slowest karma accumulation by a transaction 𝜎 𝑙

Figure 6 :

 6 Figure 6: Fastest karma accumulation by a transaction 𝜎𝑤

Figure 7 :

 7 Figure 7: Worst-case contention case for a fast accumulation karma transaction 𝜎𝑤

Figure 8 :

 8 Figure 8: Illustration of the proof of Theorem 5.5 (cases ii.c and ii.d.1)

Figure 9 :

 9 Figure 9: Illustration of the proof of Theorem 5.5 (cases ii.d.3 and ii.d.4)

Table 1 :

 1 • ∃𝜎𝑒 ∈ Enemies 𝑖 : 𝑘 𝑖 ≤ 𝑘𝑒: 𝜎 𝑖 sleeps for ∆𝑤 time units. Meanwhile, if a transaction from Enemies 𝑖 commits then 𝜎 𝑖 aborts, and if every transaction from Enemies 𝑖 aborts, then 𝜎 𝑖 commits. At the end of its sleeping period, if 𝜎𝑒 is still active, then 𝜎 𝑖 sleeps again only if its maximum number of sleeping periods 𝑤 max 𝑖,𝑒 = Notations used in this paper 𝑘𝑒-𝑘 𝑖 is not reached. The sleeping time ∆𝑤 is randomly drawn from an interval growing exponentially with each sleeping period, such that ∆𝑤 ∈ 1, 2 𝑤 𝑖,𝑒 , where 𝑤 𝑖,𝑒 is the number of achieved sleeping periods. If 𝑤 𝑖,𝑒 ≥ 𝑤 max 𝑖,𝑒 and 𝜎𝑒 is still active, then 𝜎𝑒 aborts and 𝜎 𝑖 commits.Consider a set of (𝑛 + 1) transactions, with 𝑛 slow readers and one fast writer. The execution scenario is illustrated in Figure4. Transaction 𝜎𝑤 writes into object 𝑜 and 𝑛 transactions read the value of this object.

	Symbol	Description
	𝜋	Core set of the system
	𝑇 𝒮	Task set of the system
	Σ	Transaction set of the system
	𝑂 𝒮	Object set of the system
	𝑂 Σ	STM-managed object set
	𝑂 Σ	Non-STM-managed object set
	𝜋𝑚	Core 𝑚 of the core set 𝜋
	𝜏 𝑖	Task 𝑖 of the task set 𝑇 𝒮
	J 𝑖,𝑗	J th job of task 𝑖
	𝜎 𝑘	Transaction 𝑘 of the transaction set Σ
	𝑂 𝑘	Private memory of transaction 𝑘
	Ω 𝑘	Dataset of transaction 𝑘
	𝑏 𝑘	Start date of transaction 𝑘
	𝜉 𝑘	Status of transaction 𝑘
	𝑘 𝑘	Karma of transaction 𝑘
	𝑡𝑛	Time instant 𝑛
	Active Σ 𝑡𝑛	Set of active transactions at time 𝑡𝑛
	Exec Σ 𝑡𝑛	Set of processing transactions at time
		𝑡𝑛
	TT	Turnaround Time

  Transaction 𝜎 𝑙 aborts. Transaction 𝜎𝑒 karma returns to zero and 𝜎 𝑙 karma is steadily increasing. According to Lemma 5.4, there exists a time instant 𝑡𝑛 > 𝑡𝑚 such that 𝜎 𝑙 reaches the karma limit, i.e. ∀𝜎𝑒 ∈ Enemies 𝑙 𝑡𝑛 : 𝑘 𝑙 > 𝑘𝑒. We refer to cases i.a and ii.d. (2) Transaction 𝜎𝑒 aborts. There are again two possible cases: • Transaction 𝜎 𝑙 also aborts. A third transaction, in conflict with both 𝜎𝑒 and 𝜎 𝑙 , commits. As a consequence, both transactions 𝜎𝑒 and 𝜎 𝑙 abort. According to Lemma 5.4, there exists a time instant 𝑡𝑛 > 𝑡𝑚 such that 𝜎 𝑙 reaches the karma limit, i.e. ∀𝜎𝑒 ∈ Enemies 𝑙 𝑡𝑛 : 𝑘 𝑙 > 𝑘𝑒. We refer to cases i.a and ii.d. • Transaction 𝜎 𝑙 is still active. Transaction 𝜎 𝑙 is allowed to commit. It contradicts Property 2. (3) 𝑤 𝑙,𝑒 < 𝑤 𝑚𝑎𝑥 𝑙,𝑒 , i.e. the number of sleeping periods of 𝜎 𝑙 , waiting for 𝜎𝑒, is not greater than the difference between the karma of 𝜎 𝑙 and 𝜎𝑒. Transaction 𝜎 𝑙 sleeps again, waiting for 𝜎𝑒. We refer to cases i.b.1, i.b.2 and i.b.4. (4) 𝑤 𝑙,𝑒 = 𝑤 𝑚𝑎𝑥 𝑙,𝑒 , the maximum number of sleeping periods is reached. Transaction 𝜎𝑒 aborts and transaction 𝜎 𝑙 commits. It contradicts Property 2.

1 )

 1 𝜎 𝑙 is necessarily timely correct: either 𝜎 𝑙 aborts (𝑘 𝑒 1 > 𝑘 𝑙 ) or 𝜎 𝑙 commits (𝑘 𝑒 2 ≤ 𝑘 𝑙 ).

											TT
												𝑤 𝑚𝑎𝑥 𝑒,𝑙 = 𝑘 𝑙 -𝑘𝑒 sleeping periods
	𝜎 𝑙 𝜎𝑒	𝜎	s t a r t	s t a r t	c h e c k	a b o r t	1 𝑠𝑡 sleeping period	r e s t a r t	a b o r t	2 𝑛𝑑 sleeping period	r e s t a r t	𝑖 𝑡ℎ sleeping period	(𝑤 𝑚𝑎𝑥 𝑒,𝑙 ) 𝑡ℎ sleeping period	r e s t a r t	a b o r t c h e c k c o m m i t
	𝑡1	𝑏𝑒	𝑏 𝑙											𝑡


Clotilde Ribaut

Karine Reybier
email: reybier@cict.fr

Olivier Reynes

Jérôme Launay

Alexis Valentin

Paul Louis Fabre

Franc ¸oise Nepveu

Electrochemical impedance spectroscopy to study physiological changes affecting the red blood cell after invasion by malaria parasites

The malaria parasite, Plasmodium falciparum, invades human erythrocytes and induces dramatic changes in the host cell. The idea of this work was to use RBC modified electrode to perform electrochemical impedance spectroscopy (EIS) with the aim of monitoring physiological changes affecting the erythrocyte after invasion by the malaria parasite. Impedance cell-based devices are potentially useful to give insight into cellular behavior and to detect morphological changes. The modelling of impedance plots (Nyquist diagram) in equivalent circuit taking into account the presence of the cellular layer, allowed us pointing out specific events associated with the development of the parasite such as (i) strong changes in the host cell cytoplasm illustrated by changes in the film capacity, (ii) perturbation of the ionic composition of the host cell illustrated by changes in the film resistance, (iii) releasing of reducer (lactic acid or heme) and an enhanced oxygen consumption characterized by changes in the charge transfer resistance and in the Warburg coefficient characteristic of the redox species diffusion. These results show that the RBC-based device may help to analyze strategic events in the malaria parasite development constituting a new tool in antimalarial research.

Introduction

The malaria parasite, Plasmodium falciparum, invades human erythrocytes and induces dramatic changes in membrane fluidity, permeability, deformability, and adhesiveness of the host cell. The 48-h developmental cycle in the erythrocyte can be divided into three distinct stages. The first one (ring to trophozoite, 0-24th hour) corresponds to the preparation of the first nuclear division. The communication and degradation pathways are slowly settled by the parasite and haemoglobin degradation begins. The second phase corresponds to the first nuclear division (early schizont, 24-30th hour), while haemoglobin degradation is increased, leading to hemozoin production by haem biocrystallization. The third phase (old and segmented schizont, 30-48th hour) corresponds to the next nuclear division and leads to erythrocyte membrane dis-ruption releasing 16-32 free merozoites ready to invade more intact red blood cells. In vitro, P. falciparum cultures can be synchronized for short periods (4 h) by the combination of selective concentration and/or lysis. Such a synchronization has allowed the analysis of various events during the cycle (differential expression of mRNA, hemozoin production, transient chemicals production, etc.). As the erythrocyte is a non-nucleated cell, a considerable number of the signals recorded in parasitized red blood cells is imputable to the parasite.

The aim of the work was to use a red blood cell-based device to monitor changes affecting the cells caused by invasion of Plasmodium. In a previous paper, we described a strategy to immobilize red blood cells onto a gold electrode (Ribaut et al., 2008b) in a reproducible manner. The idea was to use the modified electrode to perform electrochemical impedance spectroscopy (EIS). Impedance cell-based sensor arrays that were first described by Giaever and Keese (1984), are potentially useful to give insight into cellular behavior, to detect morphological changes (Arndt et al., 2004;Yang et al., 2007), to study cell adhesion (De Blasio et al., 2004) attachment and spreading (Xiao et al., 2002;Luong et al., 2001;Ehret et al., 1997), alterations of the physiological state or to test the efficiency of drugs (Otto et al., 2004) or effectors [START_REF] Tlili | [END_REF][START_REF] Tiruppathi | Proc. Natl. Acad. Sci[END_REF]Nguyen et al., 2004;Xiao and Luong, 2003) (environmental sensing). The physical background to the technique is based on the electrically insulating effect of cell membranes at low frequencies. The cellular sensing method allows real-time monitoring of cells, avoids the use of labelled molecules and does not interfere with cell metabolism in vitro.

In this paper, we apply for the first time, electrochemical impedance spectroscopy (EIS) to the red blood cell (RBC) with the aim of monitoring the physiological changes affecting the cell after invasion by the malaria parasite. The first part of this paper briefly describes the immobilization process whereas the second part concerns the differentiation between healthy and parasitized red blood cells by EIS.

Materials and methods

Materials

11-Mercaptoundecanoic acid (MUA), 6-mercapto-1-hexanol (MH), N-hydroxysuccinimide (NHS), N-ethyl-N ′ -(dimethylaminopropyl)-carbodiimide (EDC), phosphate buffered saline and protein G solution were purchased from Sigma-Aldrich. The anti-D (IgG) antibody Lorisix was supplied by Eurobio and absolute ethanol from Fisher Scientific. Ultrapure water was obtained using a Milli-Q water system (Simplicity, Millipore). RPMI 1640 was purchased from BioWhittaker. Red blood cells (RBC) and human serum AB + were provided by the EFS (Etablissement Franc ¸ais du Sang, Toulouse, France) and Hepes were from Lonza.

Methods

Electrode manufacturing process

The microelectrodes were designed using microelectronic mass fabrication processes as described in previous paper by metallization of pyrex wafer (Ribaut et al., 2008b). Hydrophobic PSX patterned micro-tanks were designed to prevent the spread of drops of aqueous solutions used for immobilization out of the sensitive surface.

Electrode modifications

The microelectrodes were prepared as previously described (Ribaut et al., 2008b). Briefly, the electrodes were modified by a self-assembled monolayer of mixed thiols (1 mM MUA/10 mM MH). After esterification of terminal groups by NHS and EDC (15 mM NHS/75 mM EDC), a layer of protein G (100 g/ml in PBS) and then a layer of anti-D (40 g/ml) were deposited on the surface.

The RBC (healthy or parasitized), suspended in serum-free RPMI 1640 medium to approximately 50% haematocrit, were deposited on the modified gold electrodes and incubated for 1.5 h at 37 • C in an atmosphere containing 5% CO 2 . The electrodes were then immersed in RPMI 1640, and immediately placed in the impedance electrochemical cell for measurements.

Parasite culture and magnetic separation

Parasites were cultured according to the method described by Trager and Jensen (1976) with modifications described by [START_REF] Benoit | [END_REF]. To enrich the in vitro cultures of Plasmodium, red blood cells were then transferred onto an LD-column placed in a Midi MACS magnet. This magnetic separation method allows an enrichment of up to 95% parasitemia (Ribaut et al., 2008a).

Electrochemical impedance spectroscopy

Electrochemical experiments were performed using a Voltalab 80 PGZ 402 and the voltamaster 4 software with a conventional three-electrode cell including a saturated calomel electrode (SCE) as the reference electrode, a gold electrode (0.255 cm 2 ) as the counter electrode and the modified gold electrode (0.053 cm 2 ) as the working electrode. The impedance spectra were recorded in culture medium (RPMI containing 12.5%, v/v of HEPES 1 M) in a frequency range from 50 kHz to 100 mHz at the free potential of the solution with an amplitude of the alternating voltage equal to 10 mV.

Results and discussion

Immobilization of red blood cells

As described in a previous paper (Ribaut et al., 2008b), a special method to graft red blood cells based on antigen/antibody crosslinking and a self-assembled monolayer (SAM) has been developed in our laboratory and has been used in these studies.

The immobilization of normal RBC was then simply performed by depositing a drop of medium containing red blood cells on the modified gold electrode. The same procedure was employed for parasitized red blood cells after a concentration step based on the magnetic properties of products generated by the infection (Ribaut et al., 2008a) since in normal cultures the parasitaemia does not exceed 8%, which was not sufficient to reveal differences between layers of healthy or parasitized RBC by impedance. The concentration process achieved a parasitaemia close to 95%, thus guaranteeing a signal characteristic of the infection. The electrodes modified by cellular layers of healthy or parasitized RBC were then used as working electrodes for electrochemical impedance spectroscopy.

Impedance spectroscopy

Impedance measurements were carried out in the frequency range 50 kHz to 100 mHz at the equilibrium potential at each stage of the modification process. Nyquist diagrams are presented in Fig. 1a. A significant difference in the impedance spectra is observed in the presence of normal or parasitized erythrocytes. Indeed, similar impedance spectra characterized by straight lines have been recorded for grafting layers, whereas the impedance spectra of the cells are more curved. At first, the spectra of the layers show a high resistance of charge transfer (around 400 M) which means that the exchange current at equilibrium was quite low and traduces the lack of redox couples. On the contrary, the spectra of the erythrocytes show a lower resistance of charge transfer. Furthermore, one can note that parasitized RBC present different properties in comparison with the normal ones.

It is important to note that considerable differences in equilibrium potentials were recorded for healthy (E eq = 60 mV ± 20 mV) or parasitized (E eq = -140 mV ± 50 mV) RBC. The equilibrium potential is a mixed potential between the different redox couples of the system electrode-medium: the most reducing and the most oxidizing species. Dioxygen O 2 is always present and must be the oxidant while the reducer may be from the RBC because without the RBC there is no exchange current. The cathodic displacement of the free potential between healthy and parasitized RBC (pRBC) implies the appearance of a new more powerful reductant while dioxygen which is always present is the oxidizer.

In order to obtain information on the electrical properties of parasitized versus normal red blood cells, impedance plots have been fitted according to the model circuit presented in Fig. 1b. The electrochemical system is described by the classical Randles circuit: as usual R s is the electrolyte resistance, Q dl is the double layer capacity (here a constant phase element), R ct is the charge transfer resistance and Z w is the Warburg impedance under non-stationary conditions. R ct traduces the easiness of electronic transfer whereas Z w represents the resistance to the mass transfer, i.e. to the diffusion. The multilayer structure of the electrode is taken into account by addition in a serial configuration of R f , resistance of the film, and Q f , capacitance of the dielectric of the film. In fact, this multilayer structure could be considered as the sum of the characteristics of each layer. For simplicity, the model shown in Fig. 1b was chosen.

The fitted plots of RBC layers are presented as a line in Fig. 1a. The corresponding electrical values obtained for experiments performed the same day with 4 modified electrodes (4 with healthy and 4 with parasitized cells) are summarized in Table 1.

The resistance R s of the electrolyte ( 470) is logically constant independently of the RBC state. The imperfect capacity of the film Q f decreases between healthy (8 F s n-1 ) and parasitized erythrocytes (4 F s n-1 ). From an electrical point of view, the capacity of the film can be considered as the sum in series of the capacity corresponding to each layer. The capacity of the film is given by the relation:

1/Q film = 1/Q SAM + 1/Q PG + 1/Q AD + 1/Q RBC . Taking into account that Q SAM , Q PG , Q AD should
be constant; a decrease in Q film corresponds to a decrease in Q RBC for parasitized RBC compared with healthy ones. The decrease originates from changes induced by the RBC infection, since after invasion, P. falciparum initiates a series of mor- phological and biochemical rearrangements within the host cell cytoplasm. The mature erythrocyte becomes among other things, as shown in Fig. 2a andb, a sack of haemoglobin with no endogenous protein export or protein synthesis machinery (Tilleya and Hanssen, 2008). The strong changes in the host cell cytoplasm and membrane may induce changes in the dielectric constant of the cellular layer, thus changing its capacity.

The resistance of the film R f decreases for parasitized RBC compared with healthy ones from 22 to 12 K. This evolution results from dramatic changes in the host cell membrane induced by the infection. To survive within a red blood cell, the malaria parasite alters the permeability of the host's plasma membrane to accomplish nutrient uptake and disposal of waste products. The pathogen permeabilizes host erythrocytes for a large variety of solutes (Ginsburg et al., 1983;Kutner et al., 1982), including organic and inorganic anions (Ginsburg and Kirk, 1998;Kirk, 2001) cations (Duranton et al., 2003;[START_REF] Kirk | [END_REF]Staines et al., 2000Staines et al., , 2001)), carbohydrates, amino acids, nucleosides and small peptides. In mammalian erythrocytes infected with malaria parasites there is a marked perturbation of the normal Na + /K + levels (Saliba et al., 2006;Staines et al., 2007) in the cytosol. As every cell, the erythrocyte maintains a high intracellular K + and low intracellular Na + concentration. The Na + /K + pump generates substantial opposing concentration gradients for both ions leading to a steady-state cytoplasmic [Na + ]-to-[K + ] ratio. Malaria parasites induce a marked perturbation of the normal Na + /K + levels in mammalian erythrocytes, with amongst other things, a progressive increase in the Na + concentration all over the cycle. The perturbation by the parasite of the ionic composition of its host cell could explain changes in the film resistance, rendering the cellular layer less insulating.

In the case of the electrochemical impedance of the Randles circuit, the imperfect capacity of the double-layer Q dl is the same for healthy and parasitized RBC (0.65 F s n-1 ) whereas the resistance of the charge transfer R ct decreases from 2 to 1 M. As i 0 = RT/nFR ct (Bard and Faulkner, 2001), a reduction of the charge transfer resistance implies an increase in the exchange current i 0 with i 0 = i ox = -i red and i ox + i red = 0 at equilibrium potential. Thus, an increase in the i 0 is necessary linked to an increase in i ox and i red . As explained above, the reduction current i red comes from the reduction of oxygen. The increase in i red is linked to the cathodic displacement of the free potential for parasitized RBC. However,

Table 1

Values of electrical components deduced from the modelling of Nyquist diagrams (Fig. 1a) according to the circuit model presented in Fig. 1b, Rs being the resistance of the solution, Q f the capacity of the film, n the roughness coefficient related to the capacity, R f the resistance of the film, Q dl the double layer capacity, Rct the charge transfer resistance and the Warburg coefficient.

Rs () Q f (F s n-1 ) n R f (k) Q dl (F s n-1 ) n Rct (M) ( s 1/2 )
Healthy RBC (4 electrodes) 470 ± 1 8 ± 0.8 0.9 ± 0.09 22 ± 10 0.65 ± 0.04 0.95 ± 0.004 2 ± 0.5 2.9 ± 1.7 × 10 5

Parazitized RBC (4 electrodes) 470 ± 1 4 ± 2 0.9 ± 0.05 12 ± 5 0.65 ± 0.02 0,9 ± 0.03 1 ± 0.6 5.7 ± 3 × 10 5 according to the Tafel law, a displacement of 200 mV of the equilibrium potential should induce an increase of i 0 by a factor of 40 for O 2 whereas in our case the current increases by only twofold, which implies that the oxygen concentration of the medium decreases for parasitized RBC compared with healthy ones. This result is in accordance with literature since Murphy et al. (1997) demonstrated that oxygen consumption was equal to 0.1 nmol/min for normal erythrocytes, whereas it reached 2.2 nmol/min in the case of Plasmodium infected cells. As far as i ox is concerned, a displacement of the equilibrium potential towards the cathodic potential implies that, on one hand, the reducing species responsible for i red is different for parasitized and normal erythrocytes, and on the other hand, the oxidation of this reducer takes place at a lower potential. This new reducer has to be found in the molecular species released by the parasite or consequent to the RBC infection. This could be lactic acid that can be oxidized into pyruvic acid. The infected erythrocyte has a 100-fold more intensive glycolytic activity than the healthy RBC to fulfil its substantial energy requirements (Elliott et al., 2001), ultimately converting glucose to lactic acid. Depending on the stage of development, parasitized red blood cells produced between 5 and 100 times more lactic acid than uninfected erythrocytes when cultured under identical conditions (Zolg et al., 1984). This enhanced activity would lead to an accumulation of lactic acid within the parasite cytosol and would threaten the osmotic stability of the cell (decrease in intracellular pH). For this reason the parasite has an efficient means of clearing lactic acid from its cytosol, leading to an increase in the lactic acid concentration in the erythrocyte. Given that measurements have been carried out for parasites at their latest stage of development, i.e. the schizont stage preceding membrane rupture, one can imagine that the extracellular medium contains low amounts of lactic acid. Another source of reducing species released by the parasite is the haem (Fe(II)). To sustain its rapid development, the parasite digests host haemoglobin. While hydrolysis of haemoglobin makes amino acids available for parasite development, this process also releases the lipophilic prosthetic group haem, which is extremely toxic to the parasite. 75% of the toxic haem is detoxified by the parasite converting into an insoluble crystalline material called hemozoin (Pagola et al., 2000;Egan et al., 2002). The remainder appears to be degraded by a non-enzymatic process which leads to an accumulation of iron in the parasite. Even if alternative detoxication pathways, including haem degradation (Loria et al., 1999) or reaction with glutathione (Ginsburg et al., 1998;Garavito et al., 2007) or oxygen peroxide may also contribute to haem detoxification, one can imagine that a small amount escapes the neutralisation processes and could be detected as a reducing species.

The Warburg coefficient , which is related to the inverse of the Warburg impedance and corresponds to the mass transfer, increases for infected cells compared with normal ones. As illustrated in Eq. ( 1) given for a simple redox couple, an increase of originates from the decrease of the concentration of the oxidant or/and reducer species.

= ox + red = RT n 2 F 2 A √ 2 1 C o D 1/2 o + 1 C R D 1/2 R (1)
In order to evaluate the contribution of the oxidant and the reducer on the Warburg coefficient , ox was calculated. Considering that [O 2 ] = 2.5 × 10 -4 M (solubility of O 2 in water at 20 • C) with a diffusion coefficient equal to 2 × 10 -5 cm 2 /s (in water at 20 • C) and that, as mentioned in a previous study, the working surface is only 2% of the naked electrode surface (surface coverage equal to 98%) (Ribaut et al., 2008b), ox = 2 × 10 5 s 1/2 for normal RBC. As = 2.9 × 10 5 s 1/2 in this case and taking into account that the calculation has been performed assuming that culture medium is equivalent to water, it seems that the reduction of O 2 predomi-nantly controls the mass transfer. This result explains the increase of with RBC infection that would originate from an increase in the O 2 consumption for parasitized RBC (39) and thus, a decrease in the oxygen concentration in the medium as mentioned above.

Conclusion

This study demonstrates for the first time the feasibility of performing EIS measurements on RBC adsorbed onto gold electrodes for the characterization of the physiological changes affecting the cells after invasion by Plasmodium falciparum. By using parasitized erythrocytes at the last stage of development, specific events taking place after the invasion, such as the permeation of the cell membrane as well as the release of reducing species and enhanced oxygen consumption seem to have been demonstrated by this technique. Integration of this device on a multiparametric sensor including ions and oxygen sensors could confirm interpretation proposed in this paper and help to the comprehension of the mechanisms taking place after invasion.

The stage is now set to examine the following applications of this new RBC-based device: (i) differentiation of parasitized versus healthy RBC at each stage of the parasite development, (ii) comparison of cell responses in presence of classical or new antimalarial drugs on healthy and infected cells, (iii) understanding the strategic events occurring during parasite development when antimalarials having well-known mechanisms of action are added. Such analyses are currently under development in our laboratory.

The results are very encouraging, since in the long-term, such cell-based device may be useful to probe other cellular models and diseases (e.g. inflammation, immunology, etc.).

Fig. 1 .

 1 Fig. 1. (a) Nyquist plots of non-Faradic impedance spectra taken in RPMI in the frequency range 100 mHz to 50 kHz with ( ) gold electrode, ( ) step I: mixed SAMs modified gold electrode, ( ) step II: addition of protein G on the thiol layer, (△) step III: blockage with anti-D, step IV: immobilization of normal ( ) or parasitized ( ) red blood cells. In the case of RBC layers, the symbols correspond to the experimental data (normal ( ) and parasitized red blood cells ( )) and the line represents the simulated spectra with the parameters calculated by FRA software from the equivalent circuit model presented in (b), where Rs corresponds to the resistance of the solution, R f to the resistance of the film, Q f to the capacity of the film, Q dl to the double layer capacity, Rct to the resistance of charge transfer and Zw to the Warburg impedance.

Fig. 2 .

 2 Fig. 2. Images (×2000) of normal (a) and parasitized (b) red blood cells both stained with Giemsa.

Acknowledgments

Severine Maurel-Chevalley and Eliane Pelissou are gratefully acknowledged for her technical assistance and knowledges in parasitology. We also thank Université Paul Sabatier and Institut de Recherche pour le Développement (IRD) for financial support.