Commit ef716952 authored by Glen Mével's avatar Glen Mével
Browse files

add CHANGELOG.txt, clean TODO.txt

parent 7845b11d
2021-06-04 (submitted revised version)
Changes which were required by the review summary:
- state the lesson to take home more explicitly (intro)
- add a bit more background about Iris and ghost state
- add background on Cosmo and views (sections 2.3 and 3.1)
- add background on the memory model of Multicore OCaml (section 3.1)
- rework and simplify existing background on logical atomicity (sections 2.2
and 4.6)
Some changes which were not required explicitly by the review summary:
- rework section 4 in a way that we hope is more legible and less technical
(present the ghost state of the queue more axiomatically: how we use it,
rather than how we build it)
- shorten an unnecessarily technical section about contention (section 3.5)
- address some more reviewer remarks (e.g. mention that language is untyped,
make it clear what theorem has been proven)
- various rewordings and fixes, some more citations
2021-03-01 (initial submission)
# vim: set ft=text tw=80 et ts=2:
2021-05-10
REM: nouvelle limite = 27 pages sans la biblio
REM: nouvelle limite = 27 pages sans la biblio (on est à 23)
À FAIRE SELON RÉPONSE AUX RAPPORTEURS:
REM: numéros de ligne = selon le commit 0093ac3 du 2021-04-23
- utiliser \begin{theorem}\end{theorem} ailleurs dans l’article
(p.ex. dans la section Pipeline)
modifications selon réponse aux rapporteurs:
- S 4.6: réécrire cette section sans écrire la preuve du début à la fin, mais
un focus sur quelques instants importants de la preuve. « tel moment de la
preuve est important parce que XXX. à ce moment, on dispose de YYY et il
faut prouver ZZZ. ça marche parce que ΩΩΩ »
- écrire (au début de la Section 4, L573):
« on prouve maintenant le théorème suivant: l’implé XXX satisfait la spec YYYY »
\begin{theorem}\end{theorem}
--> FAIT mais il faudra peut-être adopter ce style ailleurs dans l’article
(e.g. dans la section pipeline)
- étoffer section pipeline
- INTRO AU MODÈLE MÉMOIRE ET À COSMO:
+ dans S 2.3:
* ne pas présenter maintenant le modèle mémoire
* préciser que le MM de M-OCaml est décrit de façon opérationnelle avec une
notion de vues [Bounding Data Races, Strong Logic]
* la notion de vues vient de la sémantique opérationnelle (donc pas spécifique
à M-OCaml)
* présenter la notion de vues, d’assertions subjectives, la règle
SPLIT-OBJ-SUBJ
+ dans S 3.1:
* présenter le modèle mémoire (sous quelle forme ?)
+ dans S 4:
* donner les triplets Cosmo pour les accès mémoire de M-OCaml
--> FAIT, j’ai mis les triplets Cosmo dans S 3.1 plutôt que S 4, ça tombe comme un cheveu sur
la soupe mais je ne vois pas comment présenter le modèle mémoire dans 3.1 sinon
- une demande sans réponse d’un rapporteur pour davantage de related work:
> C "The general approach to specifying weak-memory data structures
> probably needs further evaluation and comparison with other approaches"
- EXPLICATION ATOMICITÉ LOGIQUE? déjà bien couvert dans S 2.2 + 4.5…
+ JH va revoir S 4.5
* on n’a pas besoin de Abort
FAIT
RELATED WORK:
- INTRO À IRIS ET À L’ÉTAT FANTÔME (au début de la S 4):
+ « c’est une manière flexible de définir une notion personnalisée de
ressource »
+ donner les règles de raisonnement (agreements, updates, etc.) réalisées par
nos morceaux d’état fantôme
+ le faire avant d’expliquer le détail des constructions qui permettent
d’obtenir ces règles
* voire supprimer ce détail?
+ rassurer le lecteur sur le fait que les explications arrivent…
+ un ghost name γ apparait dans 2.2, sans explication. ajouter un pointeur en avant?
- S 4.6: réécrire cette section sans écrire la preuve du début à la fin, mais un
focus sur quelques instants importants de la preuve. « tel moment de la preuve
est important parce que XXX. à ce moment, on dispose de YYY et il faut prouver
ZZZ. ça marche parce que ΩΩΩ »
+ REM: forme: le gros triplet au début de 4.6 (L864): le haut du crochet est
collé à la ligne du triplet, il faut ajouter de l’espace vertical
- incorporer ces explications dans l’article (si pas déjà présent): « The
specification of the queue in a strong (SC) memory model is of little use in
a weak memory setting. Indeed, first, the isQueue representation predicate is
difficult to share among threads unless we have stated that it is objective.
Second, with no happens-before relationship, the specification would not allow
transferring ownership of complex values (which include pieces of memory)
through the queue. In particular, the pipeline example would not be provable.
»
+ S 2.3: placer le paragraphe L339-346 avant le paragraphe qui précède (L285).
« la relation hb qu’on a établie en SC fonctionne mais est insuffisante si
on veut transférer des structures de données complexes dans la queue; la
notion qu’on voudrait, c’est d’être linéarisable, cependant notre structure
est plus faible que ce à quoi on pourrait s’attendre, on garde seulement les
hb 1, 2, 3 »
=> Fait par JH
- ÉTOFFER SECTION PIPELINE
- ÉTOFFER RELATED WORK
=> Fait
--------------------------------------------------------------------------------
2021-04
relecture par les rapporteurs ICFP…
# REMARQUES SANS RÉPONSE DANS LE REBUTTAL
C "The general approach to specifying weak-memory data structures
probably needs further evaluation and comparison with other approaches"
D "While the paper compares its results against [Vindum and Birkedal,
2021], I would have appreciated a more detailed explanation on the
differences between the different data structures used in the two
systems (Reloc and Cosmo), and salient differences between the two
systems (if any), generally, outside the specific support for weak memory."
--> deux demandes pour davantage de related work. il faudrait peut-être
répondre à ça.
--------------------------------------------------------------------------------
2021-03-08:
- écrire la comparaison détaillée avec Folly
--------------------------------------------------------------------------------
2021-03-03
RELECTURE:
intro:
- contenu: dans l’intro on insiste que l’atomicité logique en mémoire faible
c’est nouveau, mais dans l’article on ne dit rien de particulier à ce sujet,
on se contente de prendre la même définition qu’en SC et de dire que ça marche
queue:
- terminologie: échanger tail et head (enfiler en tête = pas logique par rapport
à la vie courante)
--------------------------------------------------------------------------------
2021-03-01
related work !!!
+ reprendre et alléger le related work de Cosmo pour la partie mémoire faible / Cosmo
+ à approfondir: preuve de struct. de données concurrentes
-> papier: Lars Birkedal et Simon Friis ont fait une preuve de queue (pas mémoire faible)
Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook’s Folly Library
une queue bornée MRMW qui ressemble beaucoup à la nôtre!! mais pas en mémoire faible
même structure que nous (algo légèrement différent) mais pas en mémoire faible
(en attente de publication)
-> papier: Lars Birkedal
https://cs.au.dk/~birke/papers/2021-ms-queue-final.pdf
......@@ -144,11 +44,6 @@ related work !!!
+ nous = 1er papier à présenter une struct de données concurrente en mémoire
faible avec de la SL ??
TODO personne qui fera le RelWork:
ajouter le Shavit dans local.bib et le citer dans l’intro de queue.tex
intro de queue.tex: traiter la remarque de FP
TODO personne qui fera le RelWork:
répondre à la question «la structure est-elle linéarisable»
le mot est-il bien défini dans la littérature
une définition ici ?
......@@ -158,25 +53,27 @@ répondre à la question «la structure est-elle linéarisable»
linéarisable = explicable par un historique totalement ordonné
séquentiellement consistante = les accès sont ordonnés par hb
REM: assertion splittable en une assertion persistante et une assertion timeless
= assertion «latérable», vocabulaire de Ralf Jung. les triplets actuellement
dans Iris ont de l’infrastructure pour supporter ça sans que l’user ait à manier
2 assertions, et sans later
--------------------------------------------------------------------------------
AUTRE:
2021-02-25
mentionner qu’implémenter naïvement une queue serait incorrect en cas de concurrence
remarque: la queue en mémoire faible est comparable aux refs atomiques, en ce
qu’elle sert de conteneur pour une valeur ET de structure de synchro
does the h-b from dequeuer k to enqueuer k+C relate to “quiescent consistency”
as described by Shavit (sect. 3.3) ?
--------------------------------------------------------------------------------
2021-01-25
remarquer qu’on n’utilise pas la synchro écrivain -> écrivain ni lecteur -> lecteur dans notre case-study pipeline
- related: écrire la comparaison détaillée avec Folly
- contenu: dans l’intro on insiste que l’atomicité logique en mémoire faible
c’est nouveau, mais dans l’article on ne dit rien de particulier à ce sujet,
on se contente de prendre la même définition qu’en SC et de dire que ça
marche
MINEUR:
- terminologie? échanger “tail” et “head” (vie courante: on ajoute en queue)
(relevé par 1 des 3 rapporteurs)
- biblio: citer Shavit dans l’intro de la section Queue
+ la synchro lecteur k → l’écrivain k+C (S 3.3) a-t-elle un rapport
avec la “quiescent consistency” décrite par Shavit ?
- remarque: la queue en mémoire faible est comparable aux refs atomiques, en ce
qu’elle sert de conteneur pour une valeur ET de structure de synchro
- remarque: dans le pipeline on n’utilise que la synchro écrivain → lecteur
- remarque? les triplets dans Iris ont de l’infrastructure pour les assertions
“laterable” (séparable en une assertion persistante et une assertion timeless)
sans que l’utilisateur ait à manier 2 assertions, et sans ▷
- forme: ajouter de l’espace vertical à l’intérieur des pré/post des triplets
verticaux car les grands crochets/accolades sont collés aux traits du triplet;
(cf p.ex Fig 5 "spec mémoire faible", ou Fig 7 "triplets de M-OCaml")
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment