MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

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

ICFP21 paper: clean up TODO.txt

parent 8c88eb47
......@@ -74,8 +74,6 @@ modifications selon réponse aux rapporteurs:
- ÉTOFFER RELATED WORK
=> Fait
- couper la plus grosse partie de S 3.5…
--------------------------------------------------------------------------------
2021-04
......@@ -96,13 +94,6 @@ 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.
# TODO
--> réparer ça:
> L232-235 (LAHoare and LAInv): Are you assuming the reader is familiar with
> the notation here?
--> présenter le modèle mémoire avec l’exemple du message-passing
--------------------------------------------------------------------------------
2021-03-08:
......@@ -116,31 +107,18 @@ systems (if any), generally, outside the specific support for weak memory."
RELECTURE:
intro:
- ref: "other such formalizations already exist in SC [Vindum]"
-> mentionner que c’est la même implé ? dit dans le related work
- 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
- contenu: bullet sur les happens-before = trop détaillé ? dit dans l’article
queue:
- terminologie: échanger tail et head (enfiler en tête = pas logique par rapport
à la vie courante)
queue-spec-sc:
- contenu: les figures sur l’atomicité logique ne sont pas référencées
et la syntaxe des invariants n’est pas expliquée (elle l’est plus loin,
dans l’exemple avec QueuePersistent Φ)
--------------------------------------------------------------------------------
2021-03-01
TODO: regarder le code de Simon Friis
référence pour la terminologie "lock-free":
la thèse de Keir Fraser, "Practical lock-freedom" (2004).
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
......@@ -191,13 +169,6 @@ dans Iris ont de l’infrastructure pour supporter ça sans que l’user ait à
mentionner qu’implémenter naïvement une queue serait incorrect en cas de concurrence
explication sur les triplets logiquement atomiques:
1. ce sont des triplets auteur desquels on peut ouvrir des invariants (point de
vue utilisateur)
2. explication sur le binder ∀: permet de parler de l’état au moment où on
ouvre l’invariant
3. définition des triplets atomiques
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
......@@ -208,17 +179,4 @@ as described by Shavit (sect. 3.3) ?
2021-01-25
- exemple simple d’application
+ ex: un processus envoyant quelques messages à un autre processus
+ ex plus compliqué: parcours de graphe? risque de prendre du temps…
* ex: dépendances de taches
+ mini-bibliothèque de réseaux de Kahn
+ pipeline: prgm avec deux fonctions f, g, prend en entrée une liste xs et
calcule f ∘ g (xs) mais f et g sont calculés par des threads différents
* utiliser fork-join
* question: comment le 2e thread sait quand s’arrêter ?
- soit les 2 threads connaissent à l’avancent la longueur
- soit utiliser une valeur sentinelle (ça complique l’invariant)
* idée: f x donne en postcondition Q (f x) et g y prend en précondition Q y
remarquer qu’on n’utilise pas la synchro écrivain -> écrivain ni lecteur -> lecteur dans notre case-study pipeline
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