La stratégie de la fourchette
Résumé
Dans cet article, on se propose d'utiliser les développements récents
de sémantique des jeux basés sur des ordres partiels pour donner une
sémantique dénotationnelle à une primitive de concurrence inspirée de
l'appel système UNIX fork. Cet appel système, lors de son invocation,
duplique le contexte d'exécution de son programme, et renvoie deux
entiers distincts permettant au programme de savoir dans quelle dent
de la fourche il se trouve.
La première contribution de cet article est de donner une sémantique
opérationnelle faisant droit au parfum opérateur de contrôle de cette
primitive qui manipule le contexte d'exécution. La seconde
contribution de ce papier est l'élaboration d'une sémantique des jeux
« vraiment concurrente » qui donne une représentation fine de
l'exécution du langage.
Cette sémantique des jeux est prouvée correcte vis-à-vis de la
sémantique opérationnelle et permet de faire un premier pas vers la
modélisation de comportements concurrents complexes en utilisant les
jeux concurrents.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...