Linearització

En gris una subhistòria lineal, els processos que comencen en b no tenen una història linealitzable perquè b0 o b1 es poden completar en qualsevol ordre abans que es produeixi b2.

En la programació concurrent, una operació (o conjunt d'operacions) és linealitzable si consisteix en una llista ordenada d'esdeveniments d'invocació i resposta, que es pot ampliar afegint esdeveniments de resposta de manera que:

1. La llista ampliada es pot tornar a expressar com un historial seqüencial (és serializable).
2. Aquest historial seqüencial és un subconjunt de la llista original no ampliada.

De manera informal, això significa que la llista d'esdeveniments no modificada és linealitzable si i només si les seves invocacions eren serialitzables, però algunes de les respostes de la programació en sèrie encara han de tornar.

En un sistema concurrent, els processos poden accedir a un objecte compartit alhora. Com que diversos processos accedeixen a un únic objecte, pot sorgir una situació en què mentre un procés accedeix a l'objecte, un altre procés canvia el seu contingut. Fer linearitzable un sistema és una solució a aquest problema. En un sistema linealitzable, encara que les operacions es superposen en un objecte compartit, cada operació sembla que es produeix de forma instantània. La linearització és una condició de correcció forta, que limita quines sortides són possibles quan diversos processos accedeixen a un objecte simultàniament. És una propietat de seguretat que garanteix que les operacions no es completin de manera inesperada o imprevisible. Si un sistema és linealitzable, permet al programador raonar sobre el sistema.

Història de la linearització

La linearització va ser introduïda per primera vegada com a model de consistència per Herlihy i Wing el 1987. Englobava definicions més restrictives d'atòmica, com ara "una operació atòmica és aquella que no pot ser (o no) interrompuda per operacions concurrents", que solen ser vagues sobre quan es considera que una operació comença i acaba.

Un objecte atòmic es pot entendre immediatament i completament a partir de la seva definició seqüencial, com un conjunt d'operacions que s'executen en paral·lel que sempre semblen produir-se una darrere l'altra; no poden sorgir incoherències. Concretament, la linearització garanteix que els invariants d'un sistema siguin observats i preservats per totes les operacions: si totes les operacions individualment conserven un invariant, el sistema en conjunt ho farà.

Definició de linearització

Un sistema concurrent consisteix en una col·lecció de processos que es comuniquen mitjançant estructures de dades o objectes compartits. La linealització és important en aquests sistemes concurrents on es pot accedir als objectes mitjançant diversos processos al mateix temps i un programador ha de ser capaç de raonar sobre els resultats esperats. L'execució d'un sistema concurrent dona lloc a un historial, una seqüència ordenada d'operacions completades.

Un historial és una seqüència d' invocacions i respostes fetes d'un objecte mitjançant un conjunt de fils o processos. Es pot considerar una invocació com l'inici d'una operació i la resposta és el final indicat d'aquesta operació. Cada invocació d'una funció tindrà una resposta posterior. Això es pot utilitzar per modelar qualsevol ús d'un objecte. Suposem, per exemple, que dos fils, A i B, intenten agafar un pany, retrocedint si ja l'han agafat. Això es modelaria com que els dos fils invoquen l'operació de bloqueig, i després els dos fils reben una resposta, un amb èxit i un altre no.

A invoca el bloqueig

B invoca el bloqueig

A rep una resposta "fallida".

B rep una resposta "èxit".

Una història seqüencial és aquella en què totes les invocacions tenen respostes immediates; és a dir, es considera que la invocació i la resposta es produeixen de manera instantània. Una història seqüencial hauria de ser trivial per raonar, ja que no té concurrència real; l'exemple anterior no era seqüencial i, per tant, és difícil de raonar. Aquí és on entra la linearització.

Una història és linealitzable si hi ha un ordre lineal $\sigma$ de les operacions realitzades de manera que:

1. Per a cada operació completada a , l'operació retorna el mateix resultat en l'execució que l'operació tornaria si cada operació es completés una per una en ordre.
2. Si una operació op ₁ es completa (obté una resposta) abans que comenci l'op ₂ (invoca), aleshores l'op ₁ precedeix l'op₂ a $\sigma$.

En altres paraules:

• les seves invocacions i respostes es poden reordenar per obtenir una història seqüencial;
• que la història seqüencial és correcta segons la definició seqüencial de l'objecte;
• si una resposta va precedir una invocació a l'historial original, encara l'ha de precedir en la reordenació seqüencial.

(Tingueu en compte que els dos primers punts aquí coincideixen amb la serialització: les operacions semblen passar en algun ordre. És l'últim punt que és exclusiu de la linearització i, per tant, és la contribució principal d'Herlihy i Wing.)