-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathcarbonneaux2018.html
More file actions
591 lines (556 loc) · 25.7 KB
/
carbonneaux2018.html
File metadata and controls
591 lines (556 loc) · 25.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="fr" xml:lang="fr">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Modular and Certified Resource-Bound Analyses</title>
<meta name="generator" content="Org mode" />
<style type="text/css">
<!--/*--><![CDATA[/*><!--*/
.title { text-align: center;
margin-bottom: .2em; }
.subtitle { text-align: center;
font-size: medium;
font-weight: bold;
margin-top:0; }
.todo { font-family: monospace; color: red; }
.done { font-family: monospace; color: green; }
.priority { font-family: monospace; color: orange; }
.tag { background-color: #eee; font-family: monospace;
padding: 2px; font-size: 80%; font-weight: normal; }
.timestamp { color: #bebebe; }
.timestamp-kwd { color: #5f9ea0; }
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
.underline { text-decoration: underline; }
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
p.verse { margin-left: 3%; }
pre {
border: 1px solid #ccc;
box-shadow: 3px 3px 3px #eee;
padding: 8pt;
font-family: monospace;
overflow: auto;
margin: 1.2em;
}
pre.src {
position: relative;
overflow: visible;
padding-top: 1.2em;
}
pre.src:before {
display: none;
position: absolute;
background-color: white;
top: -10px;
right: 10px;
padding: 3px;
border: 1px solid black;
}
pre.src:hover:before { display: inline;}
/* Languages per Org manual */
pre.src-asymptote:before { content: 'Asymptote'; }
pre.src-awk:before { content: 'Awk'; }
pre.src-C:before { content: 'C'; }
/* pre.src-C++ doesn't work in CSS */
pre.src-clojure:before { content: 'Clojure'; }
pre.src-css:before { content: 'CSS'; }
pre.src-D:before { content: 'D'; }
pre.src-ditaa:before { content: 'ditaa'; }
pre.src-dot:before { content: 'Graphviz'; }
pre.src-calc:before { content: 'Emacs Calc'; }
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
pre.src-fortran:before { content: 'Fortran'; }
pre.src-gnuplot:before { content: 'gnuplot'; }
pre.src-haskell:before { content: 'Haskell'; }
pre.src-hledger:before { content: 'hledger'; }
pre.src-java:before { content: 'Java'; }
pre.src-js:before { content: 'Javascript'; }
pre.src-latex:before { content: 'LaTeX'; }
pre.src-ledger:before { content: 'Ledger'; }
pre.src-lisp:before { content: 'Lisp'; }
pre.src-lilypond:before { content: 'Lilypond'; }
pre.src-lua:before { content: 'Lua'; }
pre.src-matlab:before { content: 'MATLAB'; }
pre.src-mscgen:before { content: 'Mscgen'; }
pre.src-ocaml:before { content: 'Objective Caml'; }
pre.src-octave:before { content: 'Octave'; }
pre.src-org:before { content: 'Org mode'; }
pre.src-oz:before { content: 'OZ'; }
pre.src-plantuml:before { content: 'Plantuml'; }
pre.src-processing:before { content: 'Processing.js'; }
pre.src-python:before { content: 'Python'; }
pre.src-R:before { content: 'R'; }
pre.src-ruby:before { content: 'Ruby'; }
pre.src-sass:before { content: 'Sass'; }
pre.src-scheme:before { content: 'Scheme'; }
pre.src-screen:before { content: 'Gnu Screen'; }
pre.src-sed:before { content: 'Sed'; }
pre.src-sh:before { content: 'shell'; }
pre.src-sql:before { content: 'SQL'; }
pre.src-sqlite:before { content: 'SQLite'; }
/* additional languages in org.el's org-babel-load-languages alist */
pre.src-forth:before { content: 'Forth'; }
pre.src-io:before { content: 'IO'; }
pre.src-J:before { content: 'J'; }
pre.src-makefile:before { content: 'Makefile'; }
pre.src-maxima:before { content: 'Maxima'; }
pre.src-perl:before { content: 'Perl'; }
pre.src-picolisp:before { content: 'Pico Lisp'; }
pre.src-scala:before { content: 'Scala'; }
pre.src-shell:before { content: 'Shell Script'; }
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
/* additional language identifiers per "defun org-babel-execute"
in ob-*.el */
pre.src-cpp:before { content: 'C++'; }
pre.src-abc:before { content: 'ABC'; }
pre.src-coq:before { content: 'Coq'; }
pre.src-groovy:before { content: 'Groovy'; }
/* additional language identifiers from org-babel-shell-names in
ob-shell.el: ob-shell is the only babel language using a lambda to put
the execution function name together. */
pre.src-bash:before { content: 'bash'; }
pre.src-csh:before { content: 'csh'; }
pre.src-ash:before { content: 'ash'; }
pre.src-dash:before { content: 'dash'; }
pre.src-ksh:before { content: 'ksh'; }
pre.src-mksh:before { content: 'mksh'; }
pre.src-posh:before { content: 'posh'; }
/* Additional Emacs modes also supported by the LaTeX listings package */
pre.src-ada:before { content: 'Ada'; }
pre.src-asm:before { content: 'Assembler'; }
pre.src-caml:before { content: 'Caml'; }
pre.src-delphi:before { content: 'Delphi'; }
pre.src-html:before { content: 'HTML'; }
pre.src-idl:before { content: 'IDL'; }
pre.src-mercury:before { content: 'Mercury'; }
pre.src-metapost:before { content: 'MetaPost'; }
pre.src-modula-2:before { content: 'Modula-2'; }
pre.src-pascal:before { content: 'Pascal'; }
pre.src-ps:before { content: 'PostScript'; }
pre.src-prolog:before { content: 'Prolog'; }
pre.src-simula:before { content: 'Simula'; }
pre.src-tcl:before { content: 'tcl'; }
pre.src-tex:before { content: 'TeX'; }
pre.src-plain-tex:before { content: 'Plain TeX'; }
pre.src-verilog:before { content: 'Verilog'; }
pre.src-vhdl:before { content: 'VHDL'; }
pre.src-xml:before { content: 'XML'; }
pre.src-nxml:before { content: 'XML'; }
/* add a generic configuration mode; LaTeX export needs an additional
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
pre.src-conf:before { content: 'Configuration File'; }
table { border-collapse:collapse; }
caption.t-above { caption-side: top; }
caption.t-bottom { caption-side: bottom; }
td, th { vertical-align:top; }
th.org-right { text-align: center; }
th.org-left { text-align: center; }
th.org-center { text-align: center; }
td.org-right { text-align: right; }
td.org-left { text-align: left; }
td.org-center { text-align: center; }
dt { font-weight: bold; }
.footpara { display: inline; }
.footdef { margin-bottom: 1em; }
.figure { padding: 1em; }
.figure p { text-align: center; }
.equation-container {
display: table;
text-align: center;
width: 100%;
}
.equation {
vertical-align: middle;
}
.equation-label {
display: table-cell;
text-align: right;
vertical-align: middle;
}
.inlinetask {
padding: 10px;
border: 2px solid gray;
margin: 10px;
background: #ffffcc;
}
#org-div-home-and-up
{ text-align: right; font-size: 70%; white-space: nowrap; }
textarea { overflow-x: auto; }
.linenr { font-size: smaller }
.code-highlighted { background-color: #ffff00; }
.org-info-js_info-navigation { border-style: none; }
#org-info-js_console-label
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
.org-info-js_search-highlight
{ background-color: #ffff00; color: #000000; font-weight: bold; }
.org-svg { width: 90%; }
/*]]>*/-->
</style>
<link rel="stylesheet" type="text/css" href="../css/stylesheet.css" />
<script type="text/javascript">
// @license magnet:?xt=urn:btih:1f739d935676111cfff4b4693e3816e664797050&dn=gpl-3.0.txt GPL-v3-or-Later
<!--/*--><![CDATA[/*><!--*/
function CodeHighlightOn(elem, id)
{
var target = document.getElementById(id);
if(null != target) {
elem.cacheClassElem = elem.className;
elem.cacheClassTarget = target.className;
target.className = "code-highlighted";
elem.className = "code-highlighted";
}
}
function CodeHighlightOff(elem, id)
{
var target = document.getElementById(id);
if(elem.cacheClassElem)
elem.className = elem.cacheClassElem;
if(elem.cacheClassTarget)
target.className = elem.cacheClassTarget;
}
/*]]>*///-->
// @license-end
</script>
</head>
<body>
<div id="content">
<h1 class="title">Modular and Certified Resource-Bound Analyses</h1>
<div id="table-of-contents">
<h2>Table des matières</h2>
<div id="text-table-of-contents">
<ul>
<li><a href="#org19d097b">Abstract</a></li>
<li><a href="#org9989d94">Introduction</a>
<ul>
<li><a href="#orga6ab203">Composants clés de l’analyse de ressources</a></li>
</ul>
</li>
<li><a href="#org600b001"><span class="todo TODO">TODO</span> Logiques d’invariants</a></li>
<li><a href="#org864ce62">Travaux connexes</a>
<ul>
<li><a href="#org615384d">Logiques de programmes</a></li>
<li><a href="#orgcdcbf49">Analyses automatique de ressources</a></li>
<li><a href="#orga8462d6">Génération d’invariants</a></li>
<li><a href="#org3a86dbd">Compilation vérifiée sensible au ressources</a></li>
</ul>
</li>
</ul>
</div>
</div>
<div id="outline-container-org19d097b" class="outline-2">
<h2 id="org19d097b">Abstract</h2>
<div class="outline-text-2" id="text-org19d097b">
<p>
La recherche de bornes statiques sur les besoins en ressources d’un programme,
ou <i>analyse de ressource</i> est justifiée par de nombreux besoins:
</p>
<dl class="org-dl">
<dt>Économie</dt><dd>On veut éviter de gâcher des ressources, et donc de l’argent,
à causes de programmes gourmands et les infrastructures qu’ils engendrent.</dd>
<dt>Sûreté</dt><dd>L’épuisement des ressources des systèmes embarqués et/ou critiques
peut mettre des vies humaines en danger. Les conditions exceptionnelles
d’épuisements de mémoire par exemple, ne sont que rarement bien géré – que le
premier qui sait que son code et ses dépendances transitives ne plantent pas
quand <code>malloc</code> échoue à allouer lance la première pierre.</dd>
<dt>Sécurité</dt><dd>Des attaques, dites par <i>analyse de consommation</i>, prennent
parti du comportement des implémentations pour mettre en défaut des
algorithmes pourtant corrects, en déduisant de l’information du temps de CPU ou
de la consommation mémoire d’un système cible.</dd>
<dt>Interaction</dt><dd>Le développeur d’un logiciel bénéficie déjà d’outils lui
permettant d’avoir un retour sur le code qu’il écrit: typage statique,
analyseurs pour des bugs courants, etc. Une information fiable et rapide sur
la consommation de son programme est utile à la programmation.</dd>
</dl>
<p>
L’approche à l’analyse de ressource développée ici se distingue par sa
<i>modularité</i> et sa <i>certification</i>. Modularité, car elle permet de séparer
l’analyse selon les composants du programme cible, d’implémenter des analyses
selon des axes orthogonaux, et de combiner les preuves automatisés et le
raisonnement manuel. Certification, car les bornes inférées sont augmentées de
certificats permettant de garantir leur validité. Ces certificats peuvent être
mis à l’épreuve par l’assistant de preuve <i>Coq</i> sans transformation préalable,
et couvrent tout aussi bien les déductions automatiques que les raisonnement
manuels mentionnés plus haut.
</p>
<p>
Les travaux de cette thèse montrent qu’il est possible d’analyser l’usage de
ressource à partir du code source tout en garantissant les bornes sur les
ressources réelles (et seulement asymptomatiques). Enfin, notre implémentation
permet des interactions riches entre l’analyseur et son utilisateur, via des
mécanismes d’annotations et d’insertions de raisonnement manuels.
</p>
</div>
</div>
<div id="outline-container-org9989d94" class="outline-2">
<h2 id="org9989d94">Introduction</h2>
<div class="outline-text-2" id="text-org9989d94">
</div>
<div id="outline-container-orga6ab203" class="outline-3">
<h3 id="orga6ab203">Composants clés de l’analyse de ressources</h3>
<div class="outline-text-3" id="text-orga6ab203">
<dl class="org-dl">
<dt>Sémantiques de coûts</dt><dd>Une <i>sémantique de coûts</i> est une description
mathématique de l’environnement d’exécution d’un programme permettant d’en
décrire le comportement et l’usage de ses ressources. Il est courant
d’utiliser plusieurs d’entre elles dans une même analyse: une pour le <i>langage
source</i> et l’autre pour le <i>langage cible</i>, par exemple. Le lien est fait par
un <i>compilateur sensible</i> à l’usage des ressources.</dd>
<dt>Compilateur sensible</dt><dd>Les compilateurs classiques permettent de faire le
lien entre deux sémantiques, mais sans garanties formelles sur leur résultat.
Il est courant de trouver des bugs dans des compilateurs industriels qui
influent sur leurs capacité à rendre compte de la consommation du code cible.
On cherche alors à produire des compilateurs <i>vérifiés formellement</i>, comme
CompCert (de <i>ANSI C</i> vers <i>assembleur PowerPC</i>). Hélas, afin d’accommoder les
contraintes fortes de vérification, d’importantes propriétés de consommation
ne sont ni modélisées ni préservées dans le code cible. Pour pallier à cela,
on peut soit restreindre l’analyse de ressource au code cible, soit développer
des <i>compilateurs sensibles à la consommation de ressources</i> capables de
garantir des traductions entre des sémantiques de coûts.</dd>
</dl>
<p>
<i><b>Digression:</b> Pourquoi vérifier les compilateurs?</i> On prends par exemple le
projet <i>Rust</i> de Mozilla. Rust est un langage fonctionnel de haut niveau sans
ramasse-miette, qui gère la mémoire grâce un système de type garantissant le
non-aliasing des objet selon les principe RAII. La chaîne de compilation
classique est Rust → C → assembleur. Mais ni CLANG ni GCC ne peuvent compiler
correctement le code C émit par le compilateur Rust, qui respecte cependant
scrupuleusement les standard.
</p>
<p>
Pourquoi ? Comme les pointeurs Rust sont tous soit en lecture seule, soit
non-aliasés, ils sont tous marqués par <code>const</code> ou <code>restrict</code> dans le code C
émit, alors que les compilateurs C ne sont rompus qu’au code utilisant ces
annotation avec parcimonie. Ils produisent alors du code objet <i>défectueux</i>. A
l’heure où ces lignes sont écrites, Rust est contraint de ne pas marquer ses
pointeurs avec <code>restrict</code>, et doit donc renoncer aux gains de performances que
son modèle mémoire devait garantir. Un comble. <i>Fin de digression.</i>
</p>
<dl class="org-dl">
<dt>Logiques formelles</dt><dd>Pour raisonner sur les sémantiques de coûts, il faut
développer des <i>logiques formelles</i> basées sur des <i>principes des raisonnement
pertinent</i> à la recherche de bornes de consommation, et ce à deux fins.
Premièrement, ces logiques permettent au programmeur d’inférer manuellement
des bornes et des annotations sur la consommation des programmes.
Deuxièmement, elles guident l’implémentation et la vérification des
compilateurs sensible au ressources.</dd>
<dt>Outillage (semi)-automatique</dt><dd>Même s’il est théoriquement impossible
d’entièrement automatiser l’analyse de ressource (c’est un problème
indécidable, par réduction du problème de l’arrêt), il est possible, et bien
sûr désirable, de créer des outils permettant de déterminer des bornes de
consommation pour grand nombre de programme. Quand l’automatisation totale
n’est pas possible, la logique formelle partagée entre l’outil et le
programmeur permet à ce dernier de combler les failles du raisonnement
automatique, et donc de maintenir les garanties sur les bornes obtenues.</dd>
<dt>Certificats</dt><dd>Les compilateurs et les analyseurs statiques sont des
programmes complexes dont la correction n’est jamais triviale (voir la
digression plus haut). Les bugs étant monnaie courante, l’obtention de vraie
garanties ne peut pas se faire à la tête de l’analyseur. Celui-ci doit générer
un <i>certificat</i>, c’est-à-dire un objet qui prouve la validité de son résultat
indépendamment de sa correction. L’outil tiers qui vérifie le certificat
devient alors le point faible de la chaîne de confiance des garanties de
consommation. Heureusement, des logiciels comme vérifiés formellement de fond
en comble comme Coq peuvent remplir ce rôle.</dd>
</dl>
</div>
</div>
</div>
<div id="outline-container-org600b001" class="outline-2">
<h2 id="org600b001"><span class="todo TODO">TODO</span> Logiques d’invariants</h2>
<div class="outline-text-2" id="text-org600b001">
<p>
Les logiques d’invariants forment un corpus théorique utile aux preuves de
corrections des algorithmes que l’on va implémenter durant le stage. Il serait
peu être bon d’y jeter un oeil ?
</p>
</div>
</div>
<div id="outline-container-org864ce62" class="outline-2">
<h2 id="org864ce62">Travaux connexes</h2>
<div class="outline-text-2" id="text-org864ce62">
</div>
<div id="outline-container-org615384d" class="outline-3">
<h3 id="org615384d">Logiques de programmes</h3>
<div class="outline-text-3" id="text-org615384d">
<p>
À la suite des travaux séminaux de Hoare, il s’est posé la question de comment
ajouter l’entrée-sortie à la <b>Logique de Hoare</b>. Les méthodes classiques se
basent sur des <i>variables auxiliaires</i> fraîches, présentes dans les pré- et post-
conditions des programmes et simulant des arguments formels. Dans la logique
d’invariants, on se passe de ces variables auxiliaires en introduisant les
arguments via des quantificateurs du formalisme logique ambiant. On note qu’au
moment de l’écriture de la thèse, cette nouvelle méthode est la seule
garantissant la de la méthode tout en ayant une gestion simple (sic.)
de la séquence et des variables auxiliaires.
</p>
<p>
Pour les preuves de <b>cohérence et complétude</b>. On note l’utilité d’utiliser les
techniques inventées par Wright et Felleisen dans <i>A Syntactic Approach to Type
Soundness</i>, notamment la préservation des types par la réduction.
</p>
<p>
Des <b>logiques de séparation quantitatives</b> ont été utilisées avec succès pour
manipuler les fonctions de potentiels dans des logiques de programmes. On note
l’existence d’outils permettant de quantifier l’usage de ressource de bytecode
JVM avec un certain succès, en se basant sur la <i>Vienna Development Method</i>.
L’article est Aspinall & al, sous la direction de Hoffman:
<a href="https://doi.org/10.1016/j.tcs.2007.09.003">https://doi.org/10.1016/j.tcs.2007.09.003</a>
</p>
</div>
</div>
<div id="outline-container-orgcdcbf49" class="outline-3">
<h3 id="orgcdcbf49">Analyses automatique de ressources</h3>
<div class="outline-text-3" id="text-orgcdcbf49">
<p>
Les travaux présentés dans cette thèses sont conçus dans la lignée de ceux de
Hoffmann, jusqu’au système <i>RAML</i> et l’article <i>Towards Automatic Resource Bound
Analysis for OCaml</i> (<a href="https://doi.org/10.1145/3093333.300984">https://doi.org/10.1145/3093333.300984</a>). On note trois
avancées sur ces travaux:
</p>
<ul class="org-ul">
<li>Nos fonctions de potentiels sont plus générales: alors que celles de RAML sont
des polynômes multi-variables, les nôtres sont des combinaisons linéaires de
fonctions de croissance très diverses. Ce formalisme est plus expressif et
permet à l’analyse de conclure sur des inductions bien-fondées plus complexes.</li>
<li>Nous permettons à l’utilisateur d’interagir avec l’analyse par le biais
d’annotations. L’introduction de logiques de programmes quantitatives et
complètes nous permet de garantir la correction des bornes établies même en
présence d’annotations utilisateur pour guider la recherche.</li>
<li>Enfin, notre système est le premier à générer effectivement des certificats
pour les bornes inférées. La possibilité existait pour des travaux précédent,
mais n’avais pas été effectivement implémentée.</li>
</ul>
<p>
Dans le monde impératif, de nombreux projets permettent d’obtenir des bornes et
des invariants de boucles, souvent sur des modèles abstraits des langages
ciblés, et parfois de manière ad-hoc. L’intérêt pour les méthodes de potentiels
est montant dans le domaine. Quelque projets notables (<i>CoFloCo</i>, <i>Loopus</i> et
<i>Rank</i> ne peuvent conclure sur les procédures récursives générales):
</p>
<table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
<colgroup>
<col class="org-left" />
<col class="org-left" />
<col class="org-left" />
</colgroup>
<thead>
<tr>
<th scope="col" class="org-left">Outil</th>
<th scope="col" class="org-left">Auteurs</th>
<th scope="col" class="org-left">Technique</th>
</tr>
</thead>
<tbody>
<tr>
<td class="org-left">CoFloCo</td>
<td class="org-left">Flores-Montoya</td>
<td class="org-left">relations de coûts</td>
</tr>
<tr>
<td class="org-left">KoAT</td>
<td class="org-left">Brockschmidt & al</td>
<td class="org-left">ré-écriture + terminaison</td>
</tr>
<tr>
<td class="org-left">Loopus</td>
<td class="org-left">Sinn, Zuleger & al</td>
<td class="org-left">contraintes sur différences</td>
</tr>
<tr>
<td class="org-left">PUBS</td>
<td class="org-left">Albert & al</td>
<td class="org-left">relations de coûts</td>
</tr>
<tr>
<td class="org-left">Rank</td>
<td class="org-left">Alias, Darte & al</td>
<td class="org-left">ré-écriture + terminaison</td>
</tr>
<tr>
<td class="org-left">SPEED</td>
<td class="org-left">Gulwani</td>
<td class="org-left">interprétation abstraite</td>
</tr>
</tbody>
</table>
<p>
Encore plus proche du métal, l’analyse de <i>Worst Case Resource Usage</i>
commerciale est bien développée, mais ne permet pas d’inférer des bornes
paramétriques, ou de vérifier la validité des annotations utilisateurs.
</p>
</div>
</div>
<div id="outline-container-orga8462d6" class="outline-3">
<h3 id="orga8462d6">Génération d’invariants</h3>
<div class="outline-text-3" id="text-orga8462d6">
<p>
L’analyse de ressource et la génération d’invariants forment un système
d’étoiles binaires: l’obtention d’invariant permet de borner l’usage de
ressource, et la génération d’invariants comprend souvent une réduction vers un
solveur externe dans l’esprit et le sillage de l’analyse de ressource. Cette
complémentarité est par exemple visible dans <i>SPEED</i>, mentionné plus haut. Plus
récemment, Kincaid & al ont combiné les registres abstraits accumulateurs et une
interprétation abstraite complexe pour inférer les invariant <i>polynomiaux</i>.
Hélas, la mise en forme fermée de ces invariants est un problème moins bien
cerné que dans le cas linéaire.
</p>
<p>
Dans tout les cas, il semble se dégager un schéma général en trois étapes de
l’analyse de programme:
</p>
<ol class="org-ol">
<li>Choix d’un « moule » pertinent pour les invariants recherchés;</li>
<li>Extraction de contraintes linéraires dans cet espace de travail;</li>
<li>Résolution par programmation linéaire.</li>
</ol>
<p>
Les « moules » des contraintes sont remplis avec les coefficients extrais des
structures syntaxiques du programme cible. La sémantique du langage cible
engendre les contraintes entre ces coefficients. La complexité de l’analyse est
sensible à la logique interne des contraintes: les contraintes
linéaires-par-morceaux avec quantificateurs ne peuvent pas être résolues en
temps polynomial (pour le moment). Hors des contraintes linéaires et assimilées,
Müller-Olm & Seild obtiennent des invariants sous forme de polynômes à degré
borné en utilisant un domaine abstrait de hauteur finie.
</p>
</div>
</div>
<div id="outline-container-org3a86dbd" class="outline-3">
<h3 id="org3a86dbd">Compilation vérifiée sensible au ressources</h3>
<div class="outline-text-3" id="text-org3a86dbd">
<p>
<i>CompCert</i> est un compilateur vérifié d’un fragment d’<i>ANSI C</i> vers l’assembleur
<i>PowerPC</i>, qui fournit des certificats garantissant la conservation de la
sémantique du code C en entrée. Les garanties de consommation de temps et de
mémoire doivent néanmoins toujours être obtenues par un autre logiciel, par
raisonnement sur le code assembleur produit – sauf pour des invariants portant
sur les états mémoires indépendamment les uns des autres. Nous avons étendu
<i>CompCert</i> avec une gestion de la pile selon de standard PowerPC, notamment en
prenant en compte sa finitude et en garantissant le non-débordement de pile des
programmes compilés.
</p>
<p>
De récents travaux ont permis de créer <i>CompCertS</i>, une version de CompCert qui
prend en compte la finitude de la mémoire. La sémantique des opération
allouantes inclut une vérification, sous hypothèses faibles, de la quantité de
RAM disponible. L’utilisateur peut alors obtenir des garanties simultanées sur
la <i>correction opérationelle</i> de son programme et la <i>sûreté</i> de son utilisation
des ressources. On contraste ceci avec notre approche, qui garantie la sûreté
et accorde à l’utilisateur le confort mental de pouvoir supposer la mémoire
suffisamment grande.
</p>
<p>
Enfin, Jost & al ont développés une sémantique quantitative pour leur langage
<i>Hume</i> et un compilateur sensible à l’usage des ressources de Hume vers
l’assembleur des micro-contrôleurs <i>Renesas M32C-85U</i>, mais sans certification
de la conservation sémantique par le compilateur.
</p>
</div>
</div>
</div>
</div>
</body>
</html>