Pr sentation V rification .pdf



Nom original: Pr_sentation_V_rification.pdfTitre: Quantitative synthesis for concurrent programsAuteur: Charly Finette

Ce document au format PDF 1.5 a été généré par LaTeX with Beamer class / pdfTeX-1.40.20, et a été envoyé sur fichier-pdf.fr le 15/04/2020 à 11:11, depuis l'adresse IP 77.206.x.x. La présente page de téléchargement du fichier a été vue 59 fois.
Taille du document: 357 Ko (16 pages).
Confidentialité: fichier public
🎗 Auteur vérifié


Aperçu du document


Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Quantitative synthesis for concurrent programs
Charly Finette

Février 2020

Charly Finette

Seminar

1 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Table of contents

1

Synthesis for concurrent program

2

Modèle pour le synthétiseur

3

Liens avec la théorie des jeux

4

Conclusion

Charly Finette

Seminar

2 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Introduction
Partial program resolution problem

Le synthétiseur doit résoudre le non-déterminisme.
Aucune condition sur la “qualité” du programme dans ce
modèle.
On ne peut pas demander au synthétiseur un programme à
la fois correct et efficace.

Charly Finette

Seminar

3 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Introduction
Partial program resolution problem

Le synthétiseur doit résoudre le non-déterminisme.
Aucune condition sur la “qualité” du programme dans ce
modèle.
On ne peut pas demander au synthétiseur un programme à
la fois correct et efficace.

Charly Finette

Seminar

3 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Introduction
Partial program resolution problem

Le synthétiseur doit résoudre le non-déterminisme.
Aucune condition sur la “qualité” du programme dans ce
modèle.
On ne peut pas demander au synthétiseur un programme à
la fois correct et efficace.

Charly Finette

Seminar

3 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Introduction
Partial program resolution optimization problem

Charly Finette

Seminar

4 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Processus
Definition
Un processus (thread) c est un tuple (Q, L, G, I, δ, p0 , q0 ) tel
que :
Q est un ensemble fini de “control locations”
L, G, I sont des ensembles de variables.
δ ensemble de transitions de la forme (q, g, a, q 0 ) avec
q, q 0 ∈ Q, g est une garde sur les variables, a est une
valuation des variables de L et G.
p0 est la valuation initiale de nos variables.
q0 est la “control location” initiale.

Charly Finette

Seminar

5 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Programme
Definition
Sk (c) ⊂ Q contient exactement les “control locations” où δ est
non-déterministe.
Definition
Un programme partiel M est un ensemble de processus qui ont
le même ensemble de variables globales G et la même valuation
initiale des variables de G.
Definition
Un programme P est un programme partiel tel que pour tout
c ∈ P, Sk (c) = ∅.

Charly Finette

Seminar

6 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Modèle de performance
Definition
Un automate de performance W est un automate muni d’une
fonction de coût γ qui donne à chaque action un coût.
On peut fixé un automate de performance à chaque architecture
de système.

l → locking
cs → context switching
m → main memory acess
Charly Finette

Seminar

7 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Valeur d’un programme partiel
Étant donné un programme P , un planificateur Sch et un
modèle de performance W , on construit un “gros automate”
Tr (P, Sch, W ) muni d’une fonction de coût γ.
On peut alors assigner une valeur à chaque 3-uplet
(P, Sch, W ), qui correspond à la valeur d’une exécution de
l’automate Tr (P, Sch, W ) et que l’on note :
ValProg(P, Sch, W, Saf etyB ).
Soit M un programme partiel, on note P l’ensemble de tous
les programmes autorisés par M . La valeur d’un programme
partiel est alors ValParProg(M, Sch, W, Saf etyB ) =
minp∈P ValProg(M, Sch, W Saf etyB )

Charly Finette

Seminar

8 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Version décisionnelle du problème

Soit λ ∈ Q, résoudre le partial program decision problem
(PPRDP), c’est déterminé si :
ValParProg(M, Sch, W, Saf etyB ) ≤ λ

Charly Finette

Seminar

9 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

ImpIn2 12 -player game graph
Definition
Un graphe de jeu stochastique à 2 joueurs avec information
imparfaite est un tuple G = (S, A, En, ∆, (S1 , S2 ), O, η, s0 ) avec :
S un ensemble fini d’états, s0 l’état initial
A un ensemble fini d’actions
En : S → 2A \{∅} associe à chaque état s, l’ensemble des
actions possibles à partir de s
∆ : S × A → D(S) fonction probabiliste
(S1 , S2 ) une partition de S, Si représentant les états du
joueur i
η : S → O avec O un ensemble d’observations.
Charly Finette

Seminar

10 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Sémantique

Un jeton est placé sur l’état initial.
A chaque étape, le joueur 2 peut observer sur quel état s
est posé le jeton. Le joueur 1 sait seulement que le jeton est
posé sur un état de η(s).
Si le jeton est placé dans un état s ∈ Si , le joueur i choisit
une action possible en s, on bouge alors le jeton selon
∆(s, a), une distribution de probabilité sur S.

Charly Finette

Seminar

11 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Example

Charly Finette

Seminar

12 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Résultats de complexité

Theorem
Étant donné un programme partiel M , un planificateur Sch, un
modèle de performance W et une condition de validité φ, on
p
construit un ImpIn2 21 -player game graphe GM
en temps
exponentielle avec un objectif LimAvg-Saf ety tel que la valeur
p
sans-mémoire de GM
est égale à
ValParProg(M, Sch, W, Saf etyB ).

Charly Finette

Seminar

13 / 14

Synthesis for concurrent program
Modèle pour le synthétiseur
Liens avec la théorie des jeux
Conclusion

Résultats de complexité

Theorem
Le problème de décision sans-mémoire des ImpIn2 12 -player
game graphe pour un objectif LimAvg-Saf ety est NP-complet.
Theorem
Le PPRDP est NEXPTIME-complet.

Charly Finette

Seminar

14 / 14


Aperçu du document Pr_sentation_V_rification.pdf - page 1/16
 
Pr_sentation_V_rification.pdf - page 2/16
Pr_sentation_V_rification.pdf - page 3/16
Pr_sentation_V_rification.pdf - page 4/16
Pr_sentation_V_rification.pdf - page 5/16
Pr_sentation_V_rification.pdf - page 6/16
 




Télécharger le fichier (PDF)


Pr_sentation_V_rification.pdf (PDF, 357 Ko)

Télécharger
Formats alternatifs: ZIP



Documents similaires


prsentationvrification
prsentationmocana
sminaire2020imd 4
soutenancememoirecharlyfinette
memoirecharlyfinette 3
laver 2