Liniarizabilitate

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 7 martie 2020; verificările necesită 2 modificări .

Liniarizabilitatea ( linearizarea în engleză  ) în programarea cu mai multe fire este o proprietate a unui program în care rezultatul oricărei execuții paralele a procedurilor (operațiilor) este echivalent cu o execuție secvențială. Pentru orice alt fir, execuția unei operații liniizabile este instantanee: operația fie nu a început, fie nu a fost finalizată.

După cum se arată [1] , liniarizarea este o proprietate locală și neblocantă. Localitatea înseamnă că dacă se dovedește liniarizarea operațiilor pentru mai multe programe separat (sau pentru operațiuni care lucrează cu diferite obiecte ale unui program), atunci programele împreună (operațiile împreună) vor fi și ele liniizabile. Într-un program liniizabil, operațiunile lansate nu necesită lansarea altor operațiuni pentru finalizarea lor. Aceasta este proprietatea de neblocare. În plus, liniizabilitatea facilitează demonstrarea proprietăților programelor care folosesc operații liniizabile, deoarece comportamentul unui program liniizabil este redus la execuții secvențiale.

Proprietatea de liniarizare este în multe feluri similară cu proprietăți precum serializabilitatea , atomicitatea și consistența secvențială .  În schimb, liniarizarea implică prezența unei specificații, în timp ce aceste proprietăți impun restricții doar programului în sine. În unele surse, termenul de atomicitate este folosit ca sinonim pentru liniarizare, în timp ce în altele înseamnă auto-liniarizare .  

Adesea, conceptul informal de siguranță a firului ( eng.  thread-safety ) este înțeles tocmai ca liniarizare.

Noțiunea de liniarizare a apărut pentru prima dată într-o lucrare din 1987 a lui Herlihy și Wing [2] ca model de consistență pentru sistemele cu organizare a obiectelor cu memorie partajată . Spre deosebire de toate celelalte sisteme, aici programele nu pot folosi direct variabile partajate, ci doar prin metode-funcții speciale (operații). Pentru aceste sisteme, liniarizarea coincide cu consistența strictă .

Problema testului de liniarizare este un caz special al problemei de testare funcțională , în care se verifică dacă programul îndeplinește cerințele funcționale pentru acesta, date sub forma unei specificații. Dar, spre deosebire de cazul general, aici specificația este necesară doar pentru execuții secvențiale.

Vezi și

Note

  1. Linearizare: o condiție de corectitudine pentru obiecte concurente
  2. Axiome pentru obiecte concurente

Link -uri