Sebastien Gambs

Marc-Olivier Killijian

Matthieu Roy

Moussa Traore

Keywords: Privacy, Location-based services, Ubiquitous computing

Recent advances in geolocated capacities, secure and verified positioning techniques, ubiquitous connectivity, as well as mobile and embedded systems, have led to the development of a plethora of Location-Based Services (LBS), personalizing the services they deliver according to the location of the user querying the service. However, the widespread use of mobile equipments, with ever increasing availability, precision, performance and connectivity have introduced the creepy feeling of being continuously monitored, in particular by the providers of the LBS. Thus, beyond the benefits they provide, users have started to be worried about the privacy breaches caused by such systems. The main objective of this paper is to discuss the privacy issues raised by LBS and the challenges of implementing privacy-preserving locationaware systems. Moreover, we also give a brief overview of positioning techniques used by LBS and we introduce the novel concept of locanym, which corresponds to a pseudonym linked to a particular location that could be used as a basis for developing privacy-preserving LBS.

INTRODUCTION

Due to the rapid advances in positioning technologies such as Global Positioning System (GPS), Global System for Mobile Communication (GSM), Radio Frequency IDentification (RFID), and WiFi (802.11b/g/n) and the widespread deployment of wireless local area networks, mobiles devices * This work is partially supported by LAAS, CNRS and ANR French national program for Security and Informatics (grant #ANR-11-INSE-010, project AMORES [1]). † Corresponding author, email: mtraore@laas.fr are often equipped with geolocated and wireless communication capacities. These recent development of ubiquitous devices have lead to the development of a new class of services known as Location-Based Services (LBS), that are tailored to the current location of the individual querying the service. LBS can access, combine, and transform contextual information, and more specifically location information, in order to personalize the service provided to the user. For instance, a LBS can be used for resource discovery (e.g., finding the closest restroom from my position1 ), path-finding (e.g., computing the shortest route to a gas station), realtime social applications (e.g., informing me about the presence of my friends in the vicinity2 ) or location-based gaming (e.g., playing with the nearest challenger).

When people use LBS to support them in their daily tasks, their position is usually acquire automatically through mobile equipments they carry with them. Thus, these systems continuously monitor and reveal information about the location of their users as the position of these mobile systems is essentially the same as the users of such system (e.g., which could be a single individual or a small group of persons such as a family). In most of the cases, the collected location data is transmitted to another system (typically a centralized server or another mobile equipment), which needs this information to provide the LBS (e.g., to generate the list of nearby restaurants3 ) or to participate to its computation (e.g., to help two people to meet at the optimal rendezvous point4 ). However, the collection and transmission of such data can also be used against the privacy of a user, either at the time of transmission (e.g., to send unwanted advertisement), or later in the future (e.g., to detect that the user has violated the speed limit while driving his car [START_REF] Freytag | Context quality and privacy -friends or rivals?[END_REF]). Moreover, inference attacks [START_REF] Gambs | Show me how you move and I will tell you who you are[END_REF] can be used to extract personal information from the observed mobility travels of an individual such as the Points Of Interests (POIs) characterizing his mobility (e.g., home, place of work or even the hospital that he often visits), to build mobility models that can predict with an high accuracy his past, current and future locations, as well as to deduce a part of his social graph by inferring that he has a social relationship with the individuals with whom he shares often the same physical location.

In order to address and mitigate these privacy issues, recently there has been a huge interest in the design of privacypreserving versions of LBSs providing high quality of service while preserving the privacy of their users. In this paper, we elaborate on how privacy can be integrated in location-aware systems through a few examples highlighting the complexity of addressing such issues. We also argue that privacy needs to be taken into account in LBS by grounding in fundamental privacy principles capturing the privacy needs of users of such systems. Additionally, we believe that addressing privacy in LBS should embed privacy protection and control mechanisms as fundamental requirements on all the levels of the system. The outline of this paper is the following. First in Section 2, we review the concepts of location-based services and secure positioning. Afterwards, in Section 3, we conduct a privacy analysis of some existing LBS. Finally, in Section 4 we define some desirable properties that any LBS should fulfill to protect the privacy of their users. We also introduce the notion of locanyms, which captures most of these privacy requirements, before concluding through an illustration on how these properties apply to a specific LBS.

LOCATION-BASED SERVICES AND SE-CURE POSITIONING

A LBS can be defined as a service that takes as input the current location of a user (generally acquired through a mobile device carried by this user) and tailors its output depending on the acquired location data. For instance, a user visiting a shopping mall may call a LBS to locate the closest shop that matches his budget and its clothing preferences. Therefore, location data are usually augmented with complementary information related to the user, thus further increasing the privacy risks. The ability to provide the user with a customized service depending on his location could also be used by companies to send targeted advertising and for billing purposes, by banks to perform authentication based on the location, and by restaurant owners to propose discount to users passing nearby. The above list is far from being exhaustive, as one could think about position-based access control in which the access to a particular resource is granted only to persons that are physically located inside a predefined perimeter. For instance, a printer or fax machine could be accessible only to persons located within a set of offices, or a pizza delivery service might first verify if the person placing the order is indeed located at the specified delivery address.

One of the first question that naturally arises when dealing with LBS is how a particular user can convince others about the validity of its current position. More precisely, the user can be viewed as a prover, who claims to be currently at a particular location, and which wants to convince a set of remote verifiers that he is indeed at the claimed position. Thereafter, we will refer to this problem as Secure Positioning or sometimes as Secure Position Verification. Secure Positioning is a fundamental problem that has to be tackled when designing a secure LBS and that can be addressed by designing a technique enabling the prover (i.e., the user) to prove its position through interactions with a group of verifiers. In the following, we review the two main families of approaches that have been proposed to tackle this problem (i.e., distance-bounding protocols and received signal strength), and we briefly discuss their pros and cons.

Distance-bounding Protocol

The approach based on Distance-Bounding Protocol (DBP) [3] (sometimes also called Time-of-Flight (TOF), Round-Trip Time (RTT) or Round Time-of-Flight (RToF)) aims at measuring the relative proximity of two devices using physical limits on information propagation speeds. A DBP protocol involves generally two participants, a prover and a verifier, and enables the verifier to place an upper bound on the physical distance separating him from the prover without requiring the assistance of a third party. The general schema of a DBP is the following: first, the verifier sends a challenge to the prover and starts his own timer. Upon reception of the challenge, the prover performs some computation (in some scheme, the computation simply consists in sending back the message [START_REF] Sastry | Secure verification of location claims[END_REF]) in order to construct the response to the received challenge and then sends it to the verifier, which stops his timer upon reception of the answer. By multiplying the elapsed time with the propagation speed of the signal (e.g., ultrasound or electromagnetic signals), the verifier can deduce an upper bound on his distance to the prover. Moreover, in addition to the DBP, it is possible to add a layer of authentication by having the prover authenticate himself to the verifier by using some secret shared between the prover and the verifier, thus proving that the entity responding to the challenge is indeed the prover that has initiated the DBP.

The security of DBP is based on the assumption that it should be impossible for the prover to send the response before receiving the challenge [3]. In addition, it is assumed that the processing time needed to compute the response upon reception of the challenge should be negligible compared to the propagation time of the message in order to estimate an accurate upper bound on the location of the prover. This requirement can be easily met for DBP based on ultrasounds in which the processing time of the prover needs to be in the order of microseconds to attain reasonable precision [START_REF] Rasmussen | Realization of rf distance bounding[END_REF]. However, in this context some security problems arise since (ultra-)sounds are not resistant to active attackers that can physically alter the signals. For instance, such an attacker can modify the medium (e.g., sound travels faster through metal than through the air) or use Radio Frequency (RF) wormholes (e.g., by retransmitting the signal using electromagnetic waves) to claim that it is closer from the verifier than he really is. Current knowledge of physics ensures that nothing can travel faster than light, and hence RF-based DBP (whose travel speed is very close to that of light) seems more robust, at least in the sense that they forbid such wormhole attacks. In this situation, the only threat left is that the attacker can claim to be further away than he really is by delaying his response. This does not contradict the main objective of the DBP that is to derive an upper (and not a lower) bound on the distance from the prover to the verifier. However, with RF-based DBP, the prover's processing time needs to be in the order of nanoseconds, which in the worst case allows a malicious prover to pretend be closer to the verifier by approximatively 15 centimeters (assuming that the malicious prover is able to process signals instantaneously).

Brands and Chaum [3] were the first to introduce the concept of DBP that can be used to verify the proximity of a device in a cryptographic manner. This seminal work has lead to the design of a following DBP from Hancke and Kuhn more appropriate for RFID tags and dealing with noisy environments [START_REF] Hancke | An rfid distance bounding protocol[END_REF], and a plethora of other protocols [2,[START_REF] Singelee | Distance bounding in noisy environments[END_REF][START_REF] Trujillo-Rasua | The Poulidor distance-bounding protocol[END_REF][START_REF] Čapkun | Sector: secure tracking of node encounters in multi-hop wireless networks[END_REF]. Despite their accuracy and well-founded security models, most DBP suffer from location privacy leakage [START_REF] Rasmussen | Location privacy of distance bounding protocols[END_REF]. More precisely, they always leak some information about the location and distance of the different communicating partners even to passive attackers that only eavesdroppes the communications.

Received Signal Strength Indicator

An approach used by several Wifi-based localization system is to measure the Received Signal Strength Indicator (RSSI) of the radio signals used. The RSSI approach is based on two observations: RF signal strength decreases 1) when the transmitter and the receiver are further apart and 2) when there are obstacles between the transmitter and the receiver. Based on these two observations, different readings of the signal strength are measured on different points of the location site and then recorded in a database. When the system receives a location query from a user, the system compares the user's current signal strength values with the values stored in the database. Based on this comparison, the system is able to deduce the most probable location of the user and returns it. In [START_REF] Paramvir | Enhancements to the radar user location and tracking system[END_REF], the authors have proposed a RF-based indoor location tracking system that processes the signal strength information at multiple base stations. Another localization system, WHAM! (Where AM I!) [START_REF] Lee | A model-based wifi localization method[END_REF], continuously records signal strengths received by a user's device, and disambiguates the current location of the user by backtracking to the user's previous locations in the floor model, eliminating candidate locations that are not likely to be reachable from its previous known locations. In [START_REF] Haeberlen | Practical robust localization over large-scale 802.11 wireless networks[END_REF], the authors describe a practical robust Bayesian method for topological localization that reduces the time required to train the localizer while keeping the localization accuracy good enough so that it can be used by an LBS. Many other RSSI schemes exist in the literature and we refer the reader to the following survey for more details [START_REF] Liu | Survey of wireless indoor positioning techniques and systems[END_REF].

Most RSSI schemes implicitly assume that the prover uses a standard and unmodified wireless card. However, it is not very difficult for an attacker to build a directional antenna that can largely increase the sending or receiving range, and therefore in this case measuring the signal strength does not lead to a good level of security. In addition, by jamming and replaying localization signals, an attacker can convince a device to be in a location different from its actual physical position [START_REF] Tippenhauer | Attacks on public wlan-based positioning systems[END_REF]. As a countermeasure, it was proposed to design a system based on collaborative localization in order to enhance the accuracy of the position estimation by leveraging and combining on the information gathered by neighboring nodes [4]. However, anonymization is a challenging task for the design of Wifi-based localization systems. Indeed, users are primarily authenticated through their MAC address in order to avoid undesirable deliveries of messages to unappropriate nodes. Instead of using the true MAC address, some systems [7] frequently and randomly change the MAC address of the node (which can be seen as pseudonym) to reduce the linkability risks.

PRIVACY ANALYSIS OF EXISTING LOCATION-BASED SERVICES

Currently, there is no universal metric to quantify location privacy that reached a consensus in the privacy community. Hence, it is sometimes difficult to compare different approaches aiming at building privacy-preserving LBS. Generally, each approach adopts its own definition of location privacy and defines its own adversary model. Figure 1 provides an overview of several protocols and compares them according to different criteria. In this section, we briefly review their main features and how they address privacy. Thereafter, we assume that the main objective of the attacker is to track the location of a mobile node and this attacker is equipped with eavesdropping capacities.

A Duress Alarm Location System (DALS) [5] was proposed in the early nineties for the sole purpose of determining users location, and therefore does not provide any data networking services or privacy protection. DALS uses RF-signal strengths to determine the location of a user similarly to RSSI localization techniques. Furthermore, DALS makes use of specialized and costly hardware, and therefore the trade-off between the deployment cost and the perceived value of this system is not compelling enough for large-scale adoption. RADAR [START_REF] Paramvir | Enhancements to the radar user location and tracking system[END_REF] was designed to overcome the limitations of DALS and can be deployed off-the-shelf over any wireless LAN technology. More precisely, RADAR used a RSSI localization technique and relies on a Viterbi-like algorithm for continuous tracking of users' location and disambiguation of candidate user locations with a precision of a few meters (2 -3 meters). With respect to privacy, continuous user tracking is a major threat as users may feel that "Big Brothers is continuously watching them". Furthermore, the communications exchanged can be eavesdropped as their content is not encrypted by default for these protocols. Another system, called WHAM! [START_REF] Lee | A model-based wifi localization method[END_REF], works similarly to RADAR, with the exception of the backtracking technique used, which improves the accuracy of the localization results but causes the same security and privacy problems as previous protocols. SkyHook [START_REF] Tippenhauer | Attacks on public wlan-based positioning systems[END_REF] differs from the previously described systems in the sense that the messages exchanged are encrypted. Therefore, location information can normally only be accessed by authorized entities. However, even if the user knows which entity should in principle be responsible for keeping his data private, he has no guarantee other than the promises of this entity that his location data will not be disclosed to other entities (e.g., for instance to a marketing company for a profiling purpose or to nearby shops for targeted advertising).

Recently, a distributed cooperative scheme for Neighbor Position Verification (NPV) [7] was proposed. It enables a node playing the role of the verifier to discover and ascertain the position of nearby nodes. The verifier can initiate the protocol at any time, by triggering interactive protocol within his 1-hop neighborhood that consists in 4 rounds of communication. The main objective of this protocol is to let the verifier collect enough information so that he can compute by himself the distances between any pair of neighboring nodes. In this protocol, the messages exchanged are made anonymous by taking advantage of the broadcast nature of the wireless medium, thus enabling nodes to record reciprocal timing information without disclosing their iden-

DALS 5
RADAR 15 WHAM ! 13 Swiss-Knife 12 Skyhook's 20 APPLAUS 23 Fiore and al 7 Un-linkability

! ! ! ! ! " " Architecture Anchor based " " " ! " ! ! Cooperative (User side) ! ! ! ! ! " " Centralized " " " " " " ! Techniques Time of Flight ! ! ! " ! ! " RSSI " " " ! " ! ! GPS ! ! ! ! " " ! PKI ! ! ! " " " " Location proofs ! ! ! ! ! " ! Mutual Authentication ! ! ! ! ! ! " Privacy-aware Low Low Low Medium Low High High Precision (cm) 300-600 200-300 # # 100 # #

Figure 1: Comparison of different localization protocols

tities. Afterwards, following a revelation message broadcasted by the verifier, nodes disclose their identities only to him through secure and authenticated messages, which also contain the anonymous timing information they have collected. Finally, the verifier uses this data to match the different timings and identities and then performs a ToFbased ranging to compute the distances between all pairs of communicating nodes in its neighborhood. From the point of view of privacy, this protocol ensures the anonymity of communication by relying on a generator of MAC address during the discovery phase in order to obfuscate the identity of the prover. However, this protocol assumes that the verifier is trusted (i.e., honest). Indeed, the verifier is granted the privilege to decide which entities are really in his proximity without requiring the help of an external trusted entity to verify the correctness of this proximity map.

In general, a system that can be used to generate a certified proof of the location of a node is called a location proof system. Zhu and Goa have proposed a privacy-preserving location proof system called APPLAUS [START_REF] Zhu | Towards privacy-preserving and colluding-resistance in location proof updating system[END_REF], which is composed of the following elements:

1. A prover is a node collecting location proofs by broadcasting when needed a location proof request to its neighboring nodes through Bluetooth communications.

2. A witness is a node that accepts to generate a location proof upon request and sends it back to the prover.

3.

A location proof server is required for storing the history of location proofs. It communicates directly with the provers when they submit their location proofs.

4. A certification authority (CA) is run by an independent trusted third party. Upon joining the location proof system, each mobile node registers with the CA and pre-loads a set of public/private key pairs before entering the network. The CA is the only entity that knows the correspondence between the real identity of a node and the pseudonyms (public keys) used by this node.

5.

A verifier is another node or an application that is authorized to verify a prover's location within a specific period of time.

When a prover needs to generate a location proof at particular time, it broadcasts a location proof request to its neighboring nodes through Bluetooth communications. Once a neighboring node agrees to provide a location proof for the prover, this node (now acting as a witness) generates a location proof and sends it back to the prover. The prover is responsible for forwarding this location proof to the location proof server. Finally, an authorized verifier can send a query that contains the real identity of the prover and a time interval. The CA first authenticates the verifier, and then converts the real identity contained in the query to its corresponding pseudonyms during that time period and retrieves their location proofs for this particular time period from the server. Changing pseudonyms on a regular basis provides two benefits. First, it protects the location privacy of each node by enhancing their unlinkability. Second, if the location proof server is compromised or monitored, it will be impossible for the attacker to identify the real source of the location proof. More precisely, the privacy of APPLAUS is ensured by the separation of trust: (1) the location proof server knows only pseudonyms and their associated locations, (2) the CA knows only the mapping between the real identity and its pseudonyms, and finally (3) the verifier only sees the authorized locations visited by a node for which he knows the real identity. The separation of trust ensures that as long as the attacker does not control more than one of the entity involved in the location proof system, it is impossible for him to learn a user's location because he does not have access to enough knowledge.

TOWARDS PRIVACY-PRESERVING LOCATION-BASED SERVICES

Location privacy can be broadly defined as the ability to prevent an unauthorized entity from learning the past, current or future locations of an individual. Based on this definition, most of LBS mentioned previously do not ensure location privacy. In order to reach this goal, we describe thereafter the desirable properties that we believe that a privacy-preserving LBS should fulfill:

1. Unlinkability and unforgeability. It should not be possible to trace and link different locations visited by a user. For instance, even if the user proves his locations at different occasions, it should be impossible to link the different location proofs being made by the same user. Similarly, a user should not be able to fool the system by forging a fake location proof.

2. Accountability and non-repudiation. The location information collected by the mobile device of a user should serve as a basis for deriving location proofs that are verifiable in order to ensure the validity of the user's position over an elapsed time.

3. Sovereignty. The LBS should empower the user with the control on how his location information is used and disseminated in the system. More precisely, users should be able to decide who can access their location information and under which restrictions.

Additionally, we think that it is important to use a distributed architecture, rather than a centralized server, in order to implement the LBS. Most of the systems described previously make use of the past location of user to increase the accuracy when predicting the current location or continuously monitor their positions. Such information is usually centralized by the LBS on a remote database server. However, if the security of this server is damaged, the privacy breach that can occur can be very important. Moreover, the computation of the positions by a central entity raises the possibility of continuously tracking users, which could also lead to a detailed profiling of the user. Therefore, to address this privacy concern, we recommend to build LBS by relying on a distributed architecture. In such an architecture, it is more difficult for an attacker to find the information about the location of a particular user since he does not have a single point of failure to attack to retrieve this information, which is scattered around the network. Moreover, a distributed architecture also preserves the privacy of users from being exposed to large companies, thus avoiding the "Big brother is watching you" syndrome. Finally, we also think that a privacy-preserving LBS should involve the devices present within the current neighborhood of a user to verify his position (collaborative behavior), in order to increase the resilience of the system against an active attacker. To encapsulate all these properties, we introduce the concept of locanym, which summarize the fundamental privacy requirements required to build a privacy-preserving LBS.

Definition 1 (Locanym)

A locanym is a geolocated version of a pseudonym tied to a particular geographical area. More precisely, it aims at deriving, from an accurate and verified positioning, a specific form of pseudonym providing the following properties: unlinkability, unforgeability, accountability, non-repudiation and In to illustrate the importance of the privacy desiderata defined previously for the design of LBS, we will consider a dynamic carpooling scenario based on locanyms. Dynamic carpooling is an urban service in which drivers are dynamically match with passengers from sub-urban to urban journeys or intra-urban journeys. Privacy is of paramount importance in such a setting as users move between places but their mobility patterns should be kept private from other entities (even from other mobile users that they periodically meet and cooperate with) as they generally do not know them and therefore cannot blindly trust them with their location data. Consider for instance the scenario in which Bob wishes to drive to a shop situated in the town's outskirts. Before starting his journey, Bob decides to switch on the carpooling application to gain some experiences points (and possibly some money). Approximately at the same period, Alice wants to go to a shopping mall located somewhere on Bob's path.

Unlinkability and unforgeability. After starting her carpool engine by activating the passenger mode, Alice cooperates with the neighboring nodes (e.g, bus or other moving nodes) to create her locanym data. By drawing on this locanym, the carpooling application will be able to connect Bob to Alice without disclosing her real identity since the locanym is derived only from her location data. In particular, the request of Alice cannot be linked to her identity before she meets physically with Bob (and vice-versa), which ensures the anonymity of the users of the carpooling system. Another issue is for Bob is to be sure of the truthfulness of the location claimed by his potential carpoolmate. Indeed, as the position of Alice is certified by her neighbors, she cannot fool the system by forging a false location proof except if a majority of her neighbors are colluding with her, which should be sufficiently difficult to achieve in a realistic mobile environment in order to ensure the security of the application. Therefore, Bob can trust the carpooling request and decided whether or not to carpool with Alice. In this situation, locanyms seem sufficient to ensure the mutual authentication between Alice and Bob when they establish their first relationship in a privacy-preserving manner.

Accountability and non-repudiation. Once the relationship is established and the two participants physically meet, the anonymity can be lifted and their identities revealed. Moreover suppose that during the carpooling trip, something bad happens to Alice because of Bob. During a police investigation if Bob denies having carpooled with her, Alice can nonetheless prove that she was with Bob during a certain period. Indeed, the location proofs collected by Alice mobile device can be used as an evidence. The accountability property can be important to prove to a third party (such as the administration of the city) that another entity (e.g., Bob) has actually participated in a carpooling activity. Moreover, the non-repudiation property, which can be obtained through a combination of locanyms and digital signatures, will also ensure that an entity cannot deny having participated to a carpooling trip to which he has previously given his explicit consent. The combination of accountability and non-repudiation can also be used by the carpooling service provider to offer some discounts to their regular users (e.g., such as a discount on their transport subscription).

Sovereignty. Continuing on the carpooling scenario, suppose that Alice does not want to carpool with Bob because on some problems during previous trips. However, as lo-canymity hides the identity of Bob, if such a concern is not managed by the carpool system, Alice may have a bad surprise when she arrives at the meeting place. Ideally it should be possible for Alice to express in her carpooling request (for instance in the form of a blacklist) that she does not want to carpool with Bob. This property is a form a sovereignty in the sense that Alice can decide with whom she wants (or not) to share her location. Therefore, locanyms must take into account privacy policies defined on location data by a particular node. These privacy policies should be customizable by the user depending of the privacy level needed in the spirit of Platform for Privacy Preferences (P3P) [6].

www.have2p.com

www.loopt.com

www.have2eat.com

www.rendevousSpot.com


The problem

Methodology Effective models of λ-calculus

Graph models Conclusions

λ-calculus models and theories

The lattice of λ-theories λ-theories form a complete lattice (λT , ⊆).

There is a continuum of λ-theories card(λT ) = 2 ℵ 0 : the set of r.e. λ-theories is dense in λT .

General aim

Understanding the structure of λT .

Remark

Few λ-theories come from syntactical considerations (λβ, λβη, BT , H * ), most come as the equational theory of a model:

N} logo The problem Methodology Effective models of λ-calculus Graph models Conclusions The conjecture(s) AIM: Investigate this conjecture Conjecture No (proper = non-syntactical) λ-calculus model belonging to the "main semantics": Continuous semantics (Scott), simplest subclass: Graph models (never extensional), Stable semantics (Berry and Girard), Strongly stable semantics (Bucciarelli and Ehrhard), can have an r.e. equational (order) theory. Recall All these models are partially ordered with a ⊥ element. logo The problem Methodology Effective models of λ-calculus Graph models Conclusions The conjecture(s) Can a proper model have an r.e. theory? logo The problem Methodology Effective models of λ-calculus Graph models Conclusions

Conclusions

The weaker conjecture for order theories is:

1 Proved for all graph models,

2

Proved for all effective models.

Concerning effective models the conjecture is:

1 Proved for the stable and strongly stable semantics.

2

Open for the continous semantics,

3

Even for the restricted case of graph models.

4

But our results cover all the models individually introduced in the literature.

Concerning graph models the conjecture is: Proved for large families of effective graph models.

logo

The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Conclusions

The weaker conjecture for order theories is:

1 Proved for all graph models,

2

Proved for all effective models.

Concerning effective models the conjecture is:

1 Proved for the stable and strongly stable semantics.

2

Open for the continous semantics,

3

Even for the restricted case of graph models.

4

But our results cover all the models individually introduced in the literature.

Concerning graph models the conjecture is: Proved for large families of effective graph models.

logo

The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Conclusions

The weaker conjecture for order theories is:

1 Proved for all graph models,

2

Proved for all effective models.

Concerning effective models the conjecture is:

1 Proved for the stable and strongly stable semantics.

2

Open for the continous semantics,

3

Even for the restricted case of graph models.

4

But our results cover all the models individually introduced in the literature.

Concerning graph models the conjecture is: Proved for large families of effective graph models.

Every (uniform) class of p.o. models: (Kerth 1995, Gouy, Bastonero 1996) represents 2 ℵ 0 λ-theories, (Salibra 2001) omits 2 ℵ 0 λ-theories.

Remark

Outline

The problem λ-calculus models and theories The conjecture(s)

Methodology

Effective models of λ-calculus Effective and weakly λ-models Can an effective λ-model have an r.e. theory? Some results We also look at order theories:

Graph models

Ord(M) = {(M, N) : M |= M N}.

Outline

The problem λ-calculus models and theories The conjecture(s)

Methodology

Effective models of λ-calculus Effective and weakly λ-models Can an effective λ-model have an r.e. theory? Some results

Graph models

More details

Effective domains An effective domain is a Scott-domain D = (D, D , d) where

d : N → K (D) is surjective such that: the relation "d n d m exists" is decidable in (m, n), the relation d k = d n d m is decidable in (n, m, k).

Computable and decidable elements

x ∈ D

Properties

M weakly effective

(i) |M| ∈ D r .e. for all M ∈ Λ o , (ii) if u ∈ D dec then u -= {N ∈ Λ o : |N| u} is co-r.e.
Proof Sketch: Weak effectivity implies that the interpretation function is computable. Then (i) and (ii) follow.

M effective

If M, N ∈ Λ o are β-normal, then:

(i) |M| ∈ D dec , hence: (ii) M -= {N ∈ Λ o : |N| |M|} is co-r.e.

, thus:

(iii) M -∩ N -= ∅ by [Visser, 1980]. 2 Eq(M) = λβ, λβη,

3 If ⊥ -= ∅ then Eq(M) is non r.e., 4
If M is stable or strongly stable then Eq(M) is non r.e.

Remark 1

T -= F -, where T ≡ λxy.x, F ≡ λxy.y .

Remark 2

If M is effective, then:

(i) ⊥ -, T -, F -are co-r.e. β-closed subsets of Λ o . (ii) T -∩ F -= ∅.
logo

The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Some results

Proof sketches

If M is an effective λ-model...

Theorem 1.

Ord(M) is non r.e.

Proof. If Ord(M) is r.e., then M -is r.e. β-closed and non-empty. Hence, Rem. 2 implies

F -= T -= Λ o . Contrad. Rem. 1! Theorem 2. Eq(M) = λβ, λβη.
Proof. Follows from Rem 2(ii) and Selinger's result, since

N ∈ T -∩ F -implies M |= N T . logo
The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Some results

Proof sketches

If M is an effective λ-model...

Theorem 3.

If ⊥ -= ∅ then Eq(M) is non r.e.,

Proof. ⊥ -Λ o is a β-closed, co-r.e. set by Rem. 2(i). Moreover ⊥ -is just 1 equivalence class! Hence Eq(M) cannot be r.e.

Theorem 4.

M stable or strongly stable implies Eq(M) non r.e.

Proof. Follows from Thm. 3 since in the stable and strongly stable semantics T -∩ F -= ⊥ -= ∅ (nearly true).

logo

The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Outline

The problem λ-calculus models and theories The conjecture(s)

Methodology

Effective models of λ-calculus Effective and weakly λ-models Can an effective λ-model have an r.e. theory? Some results

Graph models

D is an infinite set, i : P f (D) × D → D is a total injection.
The underlying reflexive cpo is (P(D), ⊆).

Furthermore: there is a "free completion" process for generating a web (and hence a graph model) from a partial pair (A, j). Ex: Engeler, P ω ,. . .

L öwenheim Skolem for graph models

For all graph models G there exists G with countable web such that Eq(G) = Eq(G ) (and Ord(G) = Ord(G )). ⇒ Wlog we can suppose D countable or even D = N.

  Most models do not have an r.e. theory: there are only countably many r.e. theories, T sensible ⇒ T non r.e., the few known theories of models (BT , H * & co.) are non-r.e. Is this question interesting? proper model M such that Eq(M) = λβ, λβη (r.e.)? Theorem (Selinger 1995) If Eq(M) = λβ, λβη then any p.o. on (M, •) is trivial on (the interpretations of) closed λ-terms.Known resultsNO! for graph models (corollary).(DiG-H-P,1995) ∃ proper model M such that Eq(M) = λβη in a weakly continuous semantics and not strictly proper!!! (BBB 98-00) ∃ strictly proper model M of System F in the Scott-continuous semantics such that Eq(M) = λβη F Typed calculus

  Note that: Ord(M) r.e. ⇒ Eq(M) r.e. (Visser 1980) If U, V ⊆ Λ o are β-closed, co-r.e. and non-empty, then U ∩ V = ∅.

G

  graph model with web (N, i). Effective domain: D = (P(N), ⊆), computable elements: r.e. subsets, decidable elements: decidable subsets. M = ((P(D), ⊆), A, λ), λ, A : [P(D) → P(D)] P(D) are defined by: λ(f ) ≡ {i(d, α) : d ∈ P f (D) and α ∈ f (d)}, A(u)(v ) ≡ {α ∈ D : (∃d ⊆ f v )i(d, α) ∈ u}.

logo The problem Methodology Effective models of λ-calculus Graph models Conclusions Methodology

	We concentrate on the following two classes of p.o.
	models:
	1	Eff = "Effective" λ-models (based on effective domains)
		Reason 1: Effective models (in our sense) are omni-present
		in the literature.
		Reason 2: The BBB model of System F, is effective in our
		sense.
	Definition
	Effective graph models
	Can a graph theory be r.e.?

2

G = Graph models (Based on (P(D), ⊆)) Reason: simplest class, deeply studied, generic (in some sense).

Effective graph models

Effective graph models Proposition

Examples: All free completions of finite partial pairs. Similar for all classes of webbed models K-models (Krivine) ⊃ Scott's and Park's models are effective. F-ilter models (Coppo-Dezani-Honsell-Longo-Barendregt), G-models (Girard's reflexive coherent spaces), H-models (Ehrhard's reflexive hypercoherences), logo The problem Methodology Effective models of λ-calculus

Graph models Conclusions

Can a graph theory be r.e.?

Can a graph theory be r.e.?

Theorem 1

There is a minimal equational/order graph theory, which happens to be the theory of a (non unique) effective model G.

Theorem 2

If G is a graph model then Ord(G) is not r.e.

Theorem 3

If G is an effective graph model generated by a partial pair finite modulo its group of automorphisms, then Eq(G) is not r.e.

Corollary

No graph model generated by a finite partial pair can have an r.e. theory.


Tyler Crain
email: tyler.crain@irisa.fr

Eleni Kanellou
email: eleni.kanellou@irisa.fr

Michel Raynal
email: raynal@irisa.fr

STM systems: Enforcing strong isolation between transactions and non-transactional code

Keywords: Transactional Memory, Strong Isolation, Atomicity mémoire transactionnelle, atomicité

Transactional memory (TM) systems implement the concept of an atomic execution unit called transaction in order to discharge programmers from explicit synchronization management. But when shared data is atomically accessed by both transaction and non-transactional code, a TM system must provide strong isolation in order to overcome consistency problems. Strong isolation enforces ordering between non-transactional operations and transactions and preserves the atomicity of a transaction even with respect to non-transactional code. This paper presents a TM algorithm that implements strong isolation with the following features: (a) concurrency control of non-transactional operations is not based on locks and is particularly efficient, and (b) any non-transactional read or write operation always terminates (there is no notion of commit/abort associated with them).

1 Introduction STM Systems. Transactional Memory (TM) [START_REF] Herlihy | Transactional memory: architectural support for lock-free data structures[END_REF][START_REF] Shavit | Software transactional memory. Software Transactional Memory[END_REF] has emerged as an attempt to allow concurrent programming based on sequential reasoning: By using TM, a user should be able to write a correct concurrent application, provided she can create a correct sequential program. The underlying TM system takes care of the correct implementation of concurrency. However, while most existing TM algorithms consider applications where shared memory will be accessed solely by code enclosed in a transaction, it still seems imperative to examine the possibility that memory is accessed both inside and outside of transactions.

Strong vs Weak Isolation. TM has to guarantee that transactions will be isolated from each other, but when it comes to transactions and non-transactional operations, there are two paths a TM system can follow: it may either act oblivious to the concurrency between transactions and non-transactional operations, or it may take this concurrency into account and attempt to provide isolation guarantees even between transactional and nontransactional operations. The first case is referred to as weak isolation while the second case is referred to as strong isolation. (This distinction of guarantees was originally made in [START_REF] Martin | Subtleties of Transactional Memory Atomicity Semantics[END_REF], where reference was made to "weak atomicity" versus "strong atomicity".)

While weak isolation violates the isolation principle of the transaction abstraction, it could nevertheless be anticipated and used appropriately by the programmer, still resulting in correctly functioning applications. This would require the programmer to be conscious of eventual race conditions between transactional and nontransactional code that can change depending on the STM system used.

Desirable Properties. In order to keep consistent with the spirit of TM principles, however, a system should prevent unexpected results from occurring in presence of race conditions. Furthermore, concurrency control should ideally be implicit and never be delegated to the programmer [START_REF] Crain | Towards a Universal Construction for Transaction-based Multiprocess Programs[END_REF][START_REF] Matveev | Towards a Fully Pessimistic STM Model[END_REF]. These are the reasons for which strong isolation is desirable. Under strong isolation, the aforementioned scenarios, where non-transactional operations violate transaction isolation, would not be allowed to happen. An intuitive approach to achieving strong isolation is to treat each non-transactional operation that accesses shared data as a "mini-transaction", i.e., one that contains a single operation. In that case, transactions will have to be consistent (see Sect. 2) not only with respect to each other, but also with respect to the non-transactional operations. However, while the concept of the memory transaction includes the possibility of abort, the concept of the non-transactional operation does not. This means that a programmer expects that a transaction might fail, either by blocking or by aborting. Non-transactional accesses to shared data, though, will usually be read or write operations, which the programmer expects to be atomic. While executing, a read or write operation is not expected to be de-scheduled, blocked or aborted.

Content of the Paper. This paper presents a TM algorithm which takes the previous issues into account. It is built on top of TM algorithm TL2 [START_REF] Dice | Transactional Locking II[END_REF], a word-based TM algorithm that uses locks. More precisely, TL2 is modified to provide strong isolation with non-transactional read and write operations. However, the algorithm is designed without the use of locks for non-transactional code, in order to guarantee that their execution will always terminate. To achieve this, two additional functions are specified, which substitute conventional read or write operations that have to be performed outside of a transaction. Possible violations of correctness under strong isolation are reviewed in Sect. 2. The TL2 algorithm is described in Sect. 3. Section 4 describes the proposed algorithm that implements strong isolation for TL2, while Sect. 5 concludes the paper by summarizing the work and examining possible applications.

Correctness and Strong Isolation

Consistency Issues. Commonly, consistency conditions for TM build on the concept of serializability [START_REF] Papadimitriou | The Serializability of Concurrent Updates[END_REF], a condition first established for the study of database transactions.

A concurrent execution of transactions is serializable, if there exists a serialization, i.e., a legal sequential execution equivalent to it. Serializability refers only to committed transactions, however, and fails to take into account the possible program exceptions that a TM transaction may cause -even if it aborts -when it observes an inconsistent state of memory.

Opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF], a stricter consistency condition for TM, requires that both committed as well as aborted transactions observe a consistent state of shared memory. This implies that in order for a concurrent execution of memory transactions to be opaque, there must exist an equivalent, legal sequential execution that includes both committed transactions and aborted transactions, albeit reduced to their read prefix. Other consistency conditions have also been proposed, such as virtual world consistency [START_REF] Imbs | A versatile STM protocol with invisible read operations that satisfies the virtual world consistency condition[END_REF]. It is weaker than opacity while keeping its spirit (i.e., it depends on both committed transactions and aborted transactions).

Transaction vs Non-transactional Code. In a concurrent environment, shared memory may occasionally be accessed by both transactions as well as non-transactional operations. Traditionally, however, transactions are designed to synchronize only with other transactions without considering the possibility of non-transactional code; a program that accesses the same shared memory both transactionally and non-transactionally would be considered incorrect. A TM system that implements opacity minimally guarantees consistency between transactional accesses, however, consistency violations may still be possible in the presence of concurrent non-transactional code. Given this, it can still be acceptable to have concurrent environments that may be prone to some types of violations, as is the case with systems that provide weak isolation [START_REF] Martin | Subtleties of Transactional Memory Atomicity Semantics[END_REF][START_REF] Shpeisman | Enforcing isolation and ordering in STM[END_REF]. Under weak isolation, transactional and non-transactional operations can be concurrent, but the programmer has to be aware of how to handle these. Interestingly, this possibility of co-existence of two different paradigms between strong and weak isolation reveals two different interpretations of transactional memory: On one hand considering TM as an implementation of shared memory, and, on the other hand, considering TM as an additional way of achieving synchronization, to be used alongside with locks, fences, and other traditional methods.

Under weak isolation, transactions are considered to happen atomically only with respect to other transactions. It is possible for non-transactional operations to see intermediate results of transactions that are still live. Conversely, a transaction may see the results of non-transactional operations that happened during the transaction's execution. If this behavior is not considered acceptable for an application, then the responsibility to prevent it is delegated to the programmer of concurrent applications for this system. However, in order to spare the programmer this responsibility, both the transactional memory algorithm as well as the non-transactional read and write operations must be implemented in a way that takes their co-existence into account. Such an implementation that provides synchronization between transactional and non-transactional code is said to provide strong isolation.

Providing Strong Isolation. There are different definitions in literature for strong isolation [START_REF] Harris | Transactional Memory, 2nd edition[END_REF][START_REF] Maessen | Store Atomicity for Transactional Memory[END_REF][START_REF] Martin | Subtleties of Transactional Memory Atomicity Semantics[END_REF]. In this paper we consider strong isolation to be the following: (a) non-transactional operations are considered as "mini" transactions which never abort and contain only a single read or write operation, and (b) the consistency condition for transactions is opacity.

This definition implies that the properties that are referred to as containment and non-interference [START_REF] Martin | Subtleties of Transactional Memory Atomicity Semantics[END_REF] are satisfied. Containment is illustrated in the left part of Fig. 1. There, under strong isolation, we have to assume that transaction T 1 happens atomically, i.e.,"all or nothing", also with respect to non-transactional operations. Then, while T 1 is alive, no non-transactional read, such as R x , should be able to obtain the value written to x by T 1 . Non-interference is illustrated in the right part of Fig. 1. Under strong isolation, non-transactional code should not interfere with operations that happen inside a transaction. Therefore, transaction T 1 should not be able to observe the effects of operations W x and W y , given that they happen concurrently with it, while no opacity-preserving serialization of T 1 , W x and W y can be found. Non-interference violations can be caused, for example, by nontransactional operations that are such as to cause the ABA problem for a transaction that has read a shared variable x. An additional feature of strong isolation, implemented in this paper, is that non-transactional read and write operations never block or abort. For this reason, it is termed terminating strong isolation. Privatization/Publication. A discussion of the co-existence of transactional and non-transactional code would not be complete without mentioning the privatization problem. An area of shared memory is privatized, when a process that modified it makes it inaccessible to other concurrent processes 1 with the purpose being that the process can then access the memory without using synchronization operations [START_REF] Spear | Privatization techniques for software transactional memory[END_REF]. A typical example of privatization would be the manipulation of a shared linked list. The removal of a node by a transaction T i , for private use, through non-transactional code, by the process that invoked T i , constitutes privatization. Then, T i is called privatizing transaction. While the privatization is not visible to all processes, inconsistencies may arise, given that for T i 's process the node is private but for other processes, the node is still seen as shared. Several solutions have been proposed for the privatization problem such as [START_REF] Afek | Efficient lock free privatization[END_REF][START_REF] Dice | Implicit privatization using private transactions[END_REF][START_REF] Scott | Delaunay Triangulation with Transactions and Barriers[END_REF]. A system that provides strong isolation has the advantage of inherently also solving the privatization problem, because it inherently imposes synchronization between transactional and non-transactional code.

A Brief Presentation of TL2

TL2, aspects of which are used in this paper, has been introduced by Dice, Shalev and Shavit in 2006 [START_REF] Dice | Transactional Locking II[END_REF]. The word-based version of the algorithm is used, where transactional reads and writes are to single memory words.

Main Features of TL2. The shared variables that a transaction reads form its read set, while the variables it updates form the write set. Read operations in TL2 are invisible, meaning that when a transaction reads a shared variable, there is no indication of the read to other transactions. Write operations are deferred, meaning that TL2 does not perform the updates as soon as it "encounters" the shared variables that it has to write to. Instead, the updates it has to perform are logged into a local list (also called redo log) and are applied to the shared memory only once the transaction is certain to commit. Read-only transactions in TL2 are considered efficient, because they don't need to maintain local copies of a read or write set and because they need no final read set validation in order to commit. To control transaction synchronization, TL2 employs locks and logical dates.

Locks and Logical Date. A lock is associated with each shared variable. When a transaction attempts to commit it first has to obtain the locks of the variables of its write set, before it can update them. Furthermore, a transaction has to check the logical dates of the variables in its read set in order to ensure that the values it has read correspond to a consistent snapshot of shared memory. TL2 implements logical time as an integer counter denoted GVC.

When a transaction starts it reads the current value of GVC into local variable, rv. When a transaction attempts to commit, it performs an increment-and-fetch on GVC, and stores the return value in local variable wv (which can be seen as a write version number or a version timestamp). Should the transaction commit, it will assign its wv as the new logical date of the shared variables in its write set. A transaction must abort if its read set is not valid. Its read set is valid if the logical date of every item in the set is less than the transaction's rv value. If, on the contrary, the logical date of a read set item is larger than the rv of the transaction, then a concurrent transaction has updated this item, invalidating the read.

Implementing Terminating Strong Isolation

A possible solution to the problem of ensuring isolation in the presence of non-transactional code consists in using locks: Each shared variable would then be associated with a lock and both transactions as well as non-transactional operations would have to access the lock before accessing the variable. Locks are already used in TM algorithms -such as TL2 itself -where it is however assumed that shared memory is only accessed through transactions. The use of locks in a TM algorithm entails blocking and may even lead a process to starvation. However, it can be argued that these characteristics are acceptable, given that the programmer accepts the fact that a transaction has a duration and that it may even fail: The fact that there is always a possibility that a transaction will abort means that the eventuality of failure to complete can be considered a part of the transaction concept.

On the contrary, when it comes to single read or write accesses to a shared variable, a non-transactional operation is understood as an event that happens atomically and completes. Unfortunately strong isolation implemented with locks entails the blocking of non-transactional read and write operations and would not provide termination.

Given that this approach would be rather counter-intuitive for the programmer (as well as possibly detrimental for program efficiency), the algorithm presented in this section provides a solution for adding strong isolation which is not based on locks for the execution of non-transactional operations. This algorithm builds on the base of TM algorithm TL2 and extends it in order to account for non-transactional operations. While read and write operations that appear inside a transaction follow the original TL2 algorithm rather closely (cheap read only transactions, commit-time locking, write-back), the proposed algorithm specifies non-transactional read and write operations that are to be used by the programmer, substituting conventional shared memory read and write operations. TM with strong isolation has also been proposed in software [START_REF] Schneider | Dynamic optimization for efficient strong atomicity[END_REF][START_REF] Shpeisman | Enforcing isolation and ordering in STM[END_REF] in hardware [START_REF] Minh | An effective hybrid transactional memory system with strong isolation guarantees[END_REF], and has been suggested to be too costly [START_REF] Dalessandro | Strong Isolation is a Weak Idea[END_REF]. This work differs from other implementations in that it is terminating and is implemented on top of a state-of-the-art STM in order to avoid too much extra cost.

Memory Set-up and Data Structures.

Memory Set-up. The underlying memory system is made up of atomic read/write registers. Moreover some of them can also be accessed by the the following two operations. The operation denoted Fetch&increment() atomically adds one to the register and returns its previous value. The operation denoted C&S() (for compare and swap) is a conditional write. C&S(x, a, b) writes b into x iff x = a. In that case it returns true. Otherwise it returns false.

The proposed algorithm assumes that the variables are of types and values that can be stored in a memory word. This assumption aids in the clarity of the algorithm description but it is also justified by the fact that the algorithm extends TL2, an algorithm that is designed to be word-based.

As in TL2, the variable GVC acts as global clock which is incremented by update transactions. Apart from a global notion of "time", there exists also a local one; each process maintains a local variable denoted time, which is used in order to keep track of when, with respect to the GVC, a non-transactional operation or a transaction was last performed by the process. This variable is then used during non-transactional operations to ensure the (strict) serialization of operations is not violated.

In TL2 a shared array of locks is maintained and each shared memory word is associated with a lock in this array by some function. Given this, a memory word directly contains the value of the variable that is stored in it. Instead, the algorithm presented here, uses a different memory set-up that does not require a lock array, but does require an extra level of indirection when loading and storing values in memory. Instead of storing the value of a variable directly to a memory word, each write operation on variable var, transactional or non-transactional, first creates an algorithm-specific structure that contains the new value of var, as well as necessary meta-data and second stores a pointer to this structure in the memory word. The memory set-up is illustrated in Fig. 2. Given the particular memory arrangement that the algorithm uses, pointers are used in order to load and store items from memory. 2T-record and NT-record. These algorithm-specific data structures are shared and can be of either two kinds, which will be referred to as T-records and NT-records. A T-record is created by a transactional write operation while an NT-record is created by a non-transactional write operation. When a read operation -be it transactional or non-transactional -accesses a shared variable it cannot know beforehand what type of record it will find. Therefore, it can be seen in the algorithm listings, that whenever a record is accessed, the operation checks its type, i.e., it checks whether it is a T-record or an NT-record (for example, line 02 in Fig. 3 contains such a check. A T-record is "of type T", while an NT-record is "of type NT").

T-record.

A T-record is a structure containing the following fields.

status This field indicates the state of the transaction that created the T-record. The state can either be LIVE, COMMITTED or ABORTED. The state is initially set to LIVE and is not set to COMMITTED until during the commit operation when all locations of the transaction's write set have been set to point to the transaction's T-records and the transaction has validated its read set. Since a transaction can write to multiple locations, the status field does not directly store the state, instead it contains a pointer to a memory location containing the state for the transaction. Therefore the status field of each T-record created by the same transaction will point to the same location. This ensures that any change to the transaction's state is immediately recognized at each record.

time The time field of a T-record contains the value of the GVC at the moment the record was inserted to memory. This is similar to the logical dates of TL2.

value This field contains the value that is meant to be written to the chosen memory location.

last During the commit operation, locations are updated to point to the committing transaction's T-records, overwriting the previous value that was stored in this location. Failed validation or concurrent non-transactional operations may cause this transaction to abort after it updates some memory locations, but before it fully commits. Due to this, the previous value of the location needs to be available for future reads. Instead of rolling back old memory values, the last field of a T-record is used, storing the previous value of this location.

NT-record. An NT-record is a structure containing the following fields.

value This field contains the value that is meant to be written to the chosen memory location.

time As in the case of T-records, the time field of NT-records also stores the value of the GVC when the write took place.

Due to this different memory structure a shared lock array is no longer needed, instead of locking each location in the write set during the commit operation, this algorithm performs a compare and swap directly on each memory location changing the address to point to one of its T-records. After a successful compare and swap and before the transactions status has been set to COMMITTED or ABORTED, the transaction effectively owns the lock on this location. Like in TL2, any concurrent transaction that reads the location and sees that it is locked (status = LIVE) will abort itself.

Transactional Read and Write Sets. Like TL2, read only transactions do not use read sets while update transactions do. The read set is made up of a set of tuples for each location read, addr, value where addr is the address of the location read and value is the value. The write set is also made up of tuples for each location written by the transaction, addr, item where addr is the location to be written and item is a T-record for this location.

Discussion.

One advantage of the TL2 algorithm is in its memory layout. This is because reads and writes happen directly to memory (without indirection) and the main amount of additional memory that is used is in the lock array. Unfortunately this algorithm breaks that and requires an additional level of indirection as well as additional memory per location. While garbage collection will be required for old T-and NT-records, here we assume automatic garbage collection such as that provided in Java, but additional solutions will be explored in future work. These additional requirements can be an acceptable trade-off given that they are only needed for memory that will be shared between transactions. In the appendix of this paper we present two variations of the algorithm that trade off different memory schemes for different costs to the transactional and non-transactional operations.

Description of the Algorithm.

The main goal of the algorithm is to provide strong isolation in such a way that the non-transactional operations are never blocked. In order to achieve this, the algorithm delegates most of its concurrency control and consistency checks to the transactional code. Non-transactional operations access and modify memory locations without waiting for concurrent transactions and it is mainly up to transactions accessing the same location to deal with ensuring safe concurrency. As a result, this algorithm gives high priority to non-transactional code.

Non-transactional Operations.

Algorithm-specific read and write operations shown in Fig. 3 must be used when a shared variable is accessed accessed outside of a transaction. This be done by hand or applied by a complier. Non-transactional Read. The operation non_transactional_read() is used to read, when not in a transaction, the value stored at addr. The operation first dereferences the pointer stored at addr (line 01). If the item is a T-record that was created by a transaction which has not yet committed then the value field cannot be immediately be read as the transaction might still abort. Also if the current process has read (or written to) a value that is more recent then the transaction (meaning the process's time field is greater or equal to the T-records time, line 03) then the transaction must be directed to abort (line 04) so that opacity and strong isolation (containment specifically) is not violated. From a T-record with a transaction that is not committed, the value from the last field is stored to a local variable (line 06) and will be returned on operation completion. Otherwise the value field of the T-or NT-record is used (line 07).

Next the process local variable time is advanced to the maximal value among its current value and the logical date of the T-or NT-record whose value was read. Finally if time was set to ∞ on line 11 (meaning the T-or NTrecord had yet to set its time), then it is updated to the GCV on line 12. The updated time value is used to prevent consistency violations. Once these book-keeping operations are finished, the local variable value is returned (line 13).

Non-transactional Write. The operation non_transactional_write() is used to write to a shared variable var by non-transactional code. The operation takes as input the address of the shared variable as well as the value to be written to it. This operation creates a new NT-record (line 14), fills in its fields (line 15) and changes the pointer stored in addr so that it references the new record it has created (line 16). Unlike update transactions, non-transactional writes do not increment the global clock variable GCV. Instead they just read GCV and set the NT-record's time value as well as the process local time to the value read (line 17 and 18). Since the GCV is not incremented, several NT-records might have the same time value as some transaction. When such a situation is recognized where a live transaction has the same time value as an NT-record the transaction must be aborted (if recognized during an NT-read operation, line 04) or perform read set validation (if during a transactional read operation, line 23 of Fig. 4). This is done in order to prevent consistency violations caused by the NT-writes not updating the GCV.

Transactional Read and Write Operations.

The transactional operations for performing reads and writes are presented in Fig. 4.

Transactional Read. The operation transactional_read() takes addr as input. It starts by checking whether the desired variable already exists in the transaction's write set, in which case the value stored there will be returned (line [START_REF] Spear | Ordering-Based Semantics for Software Transactional Memory[END_REF]. If the variable is not contained in the write set, the pointer in addr is dereferenced (line 20) and set to tmp. Once this is detected to be a T-or NT-record some checks are then performed in order to ensure correctness.

In the case that tmp is a T-record the operation must check to see if the status of the transaction for this record is still LIVE and if it is the current transaction is aborted (line 29). This is similar to a transaction in TL2 aborting itself when a locked location is found. Next the T-record's time field is checked, and (similar to TL2) if it greater then the process's local rv value the transaction must abort (line 32) in order to prevent consistency violations. If this succeeds without aborting then the local variable value is set depending on the stats of the transaction that created the T-record (line 29-30).

In case tmp is an NT-record (line 21), the operation checks whether the value of the time field is greater or equal to the process local rv value. If it is, then this write has possibly occurred after the start of this transaction and there are several possibilities. In the case of an update transaction validation must be preformed, ensuring that none of the values it has read have been updated (line 23). In the case of a read only transaction, the transaction is aborted and restarted as an update transaction (line 24). It is restarted as an update transaction so that it has a read set that it can validate in case this situation occurs again. Finally local variable value is set to be the value of the value field of the tmp (line 26).

It should be noted that the reason why the checks are performed differently for NT-records and T-records is because the NT-write operations do not update the global clock value while update transaction do. This means that the checks must be more conservative in order to ensure correctness. If performing per value validation or restarting the transaction as an update transaction is found to be too expensive, a third possibility would be to just increment the global clock, then restart the transaction as normal.

Finally to finish the read operation, the addr, value is added to the read set if the transaction is an update transaction (line 34), and the value of the local variable value is returned. After performing all required read and write operations, a transaction tries to commit, using the operation try_to_commit(). Similar to TL2, a try_to_commit() operation starts by trivially committing if the transaction was a read-only one (line 44) while an update transaction must announce to concurrent operations what locations it will be updating (the items in the write set). However, the algorithm differs here from TL2, given that it is faced with concurrent non-transactional operations that do not rely on locks and never block. This implies that even after acquiring the locks for all items in its write set, a transaction could be "outrun" by a non-transactional operation that writes to one of those items causing the transaction to be required to abort in order to ensure correctness. As described previously, while TL2 locks items in its write set using a lock array, this algorithm compare and swaps pointers directly to the T-records in its write set (lines 45-53) while keeping a reference to the previous value. The previous value is stored in the T-record before the compare and swap is performed (lines 48-49) with a failed compare and swap resulting in the abort of the transaction. If while performing these compare and swaps the transaction notices that another LIVE transaction is updating this memory, it aborts itself (line 48). By using these T-records instead of locks concurrent operations have access to necessary metadata used to ensure correctness.

The operation then advances the GVC, taking the new value of the clock as the logical time for this transaction (line 54). Following this, the read set of the transaction is validated for correctness (line 54). Once validation has been performed the operation must ensure that non of its writes have been concurrently overwritten by non-transactional operations (lines 55-58) if so then the transaction must abort in order to (line 57) to ensure consistency. During this check the transaction updates the time value of its T-records to the transactions logical time (line 56) similar to the way TL2 stores time values in the lock array so that future operations will know the serialization of this transaction's updates.

Finally the transaction can mark its updates as valid by changing its status variable from LIVE to COMMIT-TED (line 59). This is done using a compare and swap as there could be a concurrent non-transactional operations Inria trying to abort the transaction. If this succeeds then the transaction has successfully committed, otherwise it must abort and restart. Transactional Helping Operations. Apart from the basic operations for starting, committing, reading and writing, a transaction makes use of helper operations to perform aborts and validate the read set. Pseudo-code for this kind of helper operations is given in Fig. 6.

Operation validate_by_value() is an operation that performs validation of the read set of a transaction. Validation fails if any location in rs is currently being updated by another transaction (line 67) or has had its changed since it was first read by the transaction (line 71) otherwise it succeeds. The transaction is immediately aborted if validation fails (lines 67, 71). Before the validation is performed the local variable rv is updated to be the current value of GVC (line 63). This is done because if validation succeeds then transaction is valid at this time with a larger clock value possibly preventing future validations and aborts.

When a transaction is aborted in the present algorithm, the status of the current transaction is set to ABORTED (line 73) and it is immediately restarted as a new transaction.

Conclusion

This paper has presented an algorithm that achieves non-blocking strong isolation "on top of" a TM algorithm based on logical dates and locks, namely TL2. In the case of a conflict between a transactional and a nontransactional operation, this algorithm gives priority to the non-transactional operation, with the reasoning that while an eventual abort or restart is part of the specification of a transaction, this is not the case for a single shared read or write operation. Due to this priority mechanism, the proposed algorithm is particularly appropriate for environments in which processes do not rely heavily on the use of especially large transactions along with nontransactional write operations. In such environments, terminating strong isolation is provided for transactions, while conventional read and write operations execute with a small additional overhead.

A Version of algorithm that does not use NT-records

This algorithm also provides wait-free NT read and write operations. The difference is that NT-records are not used. Instead NT values are read and written directly from memory. By doing this, memory allocations are not needed in NT writes and NT reads have one less level of indirection.

The cost of this is more frequent validations required in transactions when conflicts with NT writes occur. This algorithm is shown in Figs. 789.

B Version of algorithm with non-blocking NT-reads and blocking NTwrites

This algorithm allows wait-free NT read operations. The only change that is needed to the base TL2 algorithm is that when an item is locked it points to the write-set of the transaction, and that each transaction has a marker that is initialized as LIVE and is set to COMMITTED just before the transaction starts performing write backs during the commit phase. The NT-read operation is shown in Fig. 10.

Figure 1 :

 1 Figure 1: Left: Containment (operation R x should not return the value written to x inside the transaction). Right: Non-Interference (wile it is still executing, transaction T 1 should not have access to the values that were written to x and y by process p 2 ).

Figure 2 :

 2 Figure 2: The memory set-up and the data structures that are used by the algorithm.

Figure 3 :

 3 Figure 3: Non-transactional operations for reading and writing a variable.

Figure 4 :

 4 Figure 4: Transactional operations for reading and writing a variable.

Figure 5 :

 5 Figure 5: Transaction begin/commit.

Figure 6 :

 6 Figure 6: Transactional helper operations.

Figure 7 :

 7 Figure 7: Non-transactional operations for reading and writing a

Figure 8 :

 8 Figure 8: Transactional operations for reading and writing a variable.

Figure 9 :

 9 Figure 9: Transaction commit.

Figure 10 :

 10 Figure 10: Non-transactional operations for reading and writing a variable.

  operation transactional_read(addr) is (19) if addr ∈ ws then return (item.value from addr in ws) end if;

	(20) tmp ← (↓ addr);
	(21) if (tmp is of type NT)
	(22)	then if (tmp.time >= rv)
	(23)	then if this is an update transaction then validate_by_value()
	(24)	else abort() and restart as an update transaction end if;
	(25)	end if;
	(26)	value ← tmp.value;
	(27)	else
	(28)	if ((status ← (↓ tmp.status)) = COMMITTED )
	(29)	then if (status = LIVE) then abort() else value ← tmp.last end if;
	(30)	else value ← tmp.value
	(31)	end if;
	(32)	if (tmp.time > rv) then abort() end if;
	(33) end if;
	(34) if this is an update transaction then add addr, value to rs end if;
	(35) return (value)
	end operation.
	operation transactional_write(addr, value) is
	(36) if addr ∈ ws
	(37)	then allocate a new variable item of type T ;
	(38)	item ← (value, (↑ status), ∞); ws ← ws ∪ addr, item ;
	(39)	else set item.value with addr in ws to value
	(40) end if;
	end operation.

  operation transactional_read(addr) is (88) if addr ∈ ws then return (item.value from addr in ws) end if; (89) tmp ← (↓ addr); (90) if (tmp is of type T ) (91) then if (status = LIVE) then abort() end if; (92) if (tmp.time > rv) then abort() end if; (101) if this is an update transaction then add value to rs end if; (102) return (value) end operation. operation transactional_write(addr, value) is (103) if addr ∈ ws (104) then allocate a new variable item of type T ; (105) item ← (addr, value, status, ∞); ws ← ws ∪ item (106) else set item.value with addr in ws to value (107) end if end operation.

	(93)	if (status = COMMITTED)
	(94)	then value ← tmp.val
	(95)	else value ← tmp.last
	(96)	end if;
	(97)	else
		% Do validation to prevent abort due to a non-transactional write
	(98)	rv ← validate_by_value();
	(99)	value ← tmp;
	(100) end if;

  Inria operation non_transactional_read(addr) is (131) lock ← load_lock(addr); (132) value ← (↓ addr); (133) if ( lock is locked ∧tmp.status = COMMITTED ∧addr ∈ lock.ws) (134) then value ← item.value from addr in lock.ws (135) end if; (136) return (value) end operation. operation non_transactional_write(addr, value) is (137) Perform a transactional begin/write/commit operation end operation.

RR n°7970

Inria

Conversely, a memory area is made public when it goes from being exclusively accessible by one process to being accessible by several processes[START_REF] Spear | Ordering-Based Semantics for Software Transactional Memory[END_REF] . This is referred to as the publication problem and the consistency issues that arise are analogous.RR n°7970

The following notation is used. If pt is a pointer, pt ↓ is the object pointed to by pt. if aa is an object, ↑ aa is a pointer to aa. Hence ((↑ aa) ↓= aa and ↑ (pt ↓) = pt.

Transactional Write. The transactional_write() operation takes addr as input value, as well as the value to be written to var. As TL2, the algorithm performs commit-time updates of the variables it writes to. For this reason, the transactional write operation simply creates a T-record and fills in some of its fields (lines 37 -38) and adds it to the write set. However, in the case that a T-record corresponding to addr was already present in the write set, the value field of the corresponding T-record is simply updated (line 39).

Begin and End of a Transaction

The operations that begin and end a transaction are begin_transaction() and try_to_commit(), presented in Fig. 5. Local variables necessary for transaction execution are initialized by begin_transaction(). This includes rv which is set to GCV and, like in TL2, is used during transactional reads to ensure correctness, as well as status which is set to LIVE and the read and write sets which are initialized as empty sets. (lines 41-43).


Laurent Vercouter
email: laurent.vercouter@insa-rouen.fr

Pierre Maret
email: pierre.maret@univ-st-etienne.fr

Introducing Web Intelligence for Communities

Introduction

The field of Web Intelligence has grown quickly in the last decade as a crossroads between the researches in Artificial Intelligence and the development of the web. In this field, communities appear as a first-class object as is found in many diverse web applications. The most popular and well known examples are social network sites for entertainement. But their success should not hide other application domains where the concept of communities is central. Education, healthcare, design, knowledge management or virtual enterprises are other domains in which communities appear and require technological support. The contribution of web technologies is obvious as the intrisic nature of the web is precisely to provide and support links between individuals. Research works related to these technologies, especially web intelligence, provide then innovative approaches and contributions to every step of the lifecycle of a community supported by the web.

Social component of communities

The main objective of forming a community is social, and a community can be seen according to three social characteristics. It is composed of participants, communication and content.

Participants

A community brings together participants sharing a same interest regarding the subject of the community. Each participant can be analyzed according to her specific profile, interests or practices. Both the mutual characteristics of participants (for instance, the motivation for which they are all included in the same community) and their differences should be considered. The fact that we consider communities deployed on the web has an impact on the nature of the participants who are not only human users, but maybe software agents. Hybrid communities composed of humans and softwares are now possible.

Communications

A common motivation of community participants is to share information, thus requiring communication facilities. Adequate communications media have to be developped and the field of Web Intelligence can provide innovative solutions. The implementation of communication protocols is obviously concerned as well as issues related to specific features of communication. These features include security properties, trust management, privacy preservation, information retrieval, . . .

Content

As explained before, there is a common motivation for individuals to participate in the same community. This motivation is often related to the content circulating inside the community. The content is often information, sometimes services, and the community exists because some content is formalized, exchanged and understood. This raises issues about content modelling, storage, discovery and exchange. Knowledge extraction is another concern mainly for the fields of machine learning or data mining as a way to analyze a community's behavior.

All these aspects can be addressed and their combinations lead to the complex first-class objects that are communities.

Papers of the special issue

The six following papers published in Number A first set of papers shows the purpose of using communities as an object of study by the way of Web Intelligence technologies. The problem consists in analysing a community as a social phenomenon in order to extract knowledge and insights.

-The analysis method proposed by Leprovost et al [START_REF] Leprovost | Discovering Implicit Communities in Web forums through Ontologies[END_REF] aims at discovering communities of interest by studying discussion forums. The identification of terms, topics or concepts that are important within a community gives interesting information about its current opinion trends. -Social networks are the specific kind of communities addressed by the paper of Forestier et al [START_REF] Forestier | Roles in social networks: methodologies and research issues[END_REF]. The analysis of community member interactions provides some insight into the organization and the roles existing in a social network in one specific case [START_REF] Forestier | Roles in social networks: methodologies and research issues[END_REF]. -Tchuente et al [START_REF]Dieudonne Tchuente and Nadine Baptiste-Jessel and Andre Peninou and Marie-Francoise Canut and Florence Sedes[END_REF] also consider that social networks are a specific kind of community.

In their approach, the analysis of interactions can be used to extract knowledge from the individuals themselves and from their social profile.

Another approach that can be found in this selection of papers concerns the development of models and tools in order to facilitate the functionning of virtual communities. The main functionality expected in a virtual community is the exchange of information and/or services.

-A self-organization of a social network is thus proposed [START_REF] Mercier | Using multiagent self-organization techniques for seeking information in virtual social communities[END_REF] to adapt a user's neighborhood to their personal preferences. -Bugeaud et al [START_REF] Bugeaud | OntoStoria2 : a shared representation and a web-based tool for the collaboration of services providers innovators[END_REF] propose another tool, called OntoStoria, to support the execution of collaborative services in a community of innovative workers. -Finally, the fact that people share personal information raises privacy problems, exacerbated by the use of web technologies and its possibilities of information access, propagation and processing. Krupa et al [START_REF] Krupa | Handling privacy as contextual integrity in decentralized virtual communities: The PrivaCIAS framework[END_REF] address this problem with a multi-agent approach to privacy preservation.

This panel of works gives concrete examples of the contributions of Web Intelligence technologies to modern applications relying on communities, both to understand their functionning and to support them. The progress of technology enables the emergence of new uses that, in turn, need to be understood and bring new technological requirements. This cyclical advance where uses and technology are interwoven constitutes the development basis of the subfield of Web Intelligence & Communities.

  1570-1263/12/$17.00 c 2012 -IOS Press and the authors. All rights reserved

1 and 2 of

 2 Volume 10 of the Web Intelligence & Agent Systems journal provide a panel of contributions related to communities in conjunction with the Internet and/or Artificial Intelligence techniques. These works attest to the recent rise of interest in the topic of Web Intelligence & Communities, leading to the creation of a dedicated workshop 1 .

http://wic.litislab.fr