Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Linearizability
Résumé
In concurrent programming, an operation (or set of operations) is linearizable if it consists of an ordered list of invocation and response events, that may be extended by adding response events such that:
The extended list can be re-expressed as a sequential history (is serializable).
That sequential history is a subset of the original unextended list.
Informally, this means that the unmodified list of events is linearizable if and only if its invocations were serializable, but some of the responses of the serial schedule have yet to return.
In a concurrent system, processes can access a shared object at the same time. Because multiple processes are accessing a single object, a situation may arise in which while one process is accessing the object, another process changes its contents. Making a system linearizable is one solution to this problem. In a linearizable system, although operations overlap on a shared object, each operation appears to take place instantaneously. Linearizability is a strong correctness condition, which constrains what outputs are possible when an object is accessed by multiple processes concurrently. It is a safety property which ensures that operations do not complete unexpectedly or unpredictably. If a system is linearizable it allows a programmer to reason about the system.
Linearizability was first introduced as a consistency model by Herlihy and Wing in 1987. It encompassed more restrictive definitions of atomic, such as "an atomic operation is one which cannot be (or is not) interrupted by concurrent operations", which are usually vague about when an operation is considered to begin and end.
An atomic object can be understood immediately and completely from its sequential definition, as a set of operations run in parallel which always appear to occur one after the other; no inconsistencies may emerge. Specifically, linearizability guarantees that the invariants of a system are observed and preserved by all operations: if all operations individually preserve an invariant, the system as a whole will.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Publications associées (1)
Personnes associées (1)
Concepts associés (36)
Compare-and-swap
Compare-and-swap (CAS) est une instruction atomique utilisée dans les systèmes multiprocesseurs ou multi-cœurs utilisant une mémoire partagée. Elle compare la valeur stockée à une adresse mémoire donnée à l'un de ses arguments et, en cas d'égalité, écrit une nouvelle valeur à cette adresse. Selon les implémentations, elle signale si l'écriture a réussi soit en renvoyant une valeur booléenne, soit en renvoyant la valeur lue en mémoire.
Programmation concurrente
La programmation concurrente est un paradigme de programmation tenant compte, dans un programme, de l'existence de plusieurs piles sémantiques qui peuvent être appelées threads, processus ou tâches. Elles sont matérialisées en machine par une pile d'exécution et un ensemble de données privées. La concurrence est indispensable lorsque l'on souhaite écrire des programmes interagissant avec le monde réel (qui est concurrent) ou tirant parti de multiples unités centrales (couplées, comme dans un système multiprocesseurs, ou distribuées, éventuellement en grille ou en grappe).
Modèle de cohérence
En Informatique, les modèles de cohérence sont utilisés dans les systèmes répartis comme les systèmes de mémoire partagée distribuée (DSM) ou les magasins de données distribuées (tels que les système de fichiers, les bases de données, les systèmes de réplication optimiste ou la mise en cache web). On dit que le système supporte un modèle donné si les opérations sur la mémoire suivent des règles spécifiques.