source: LTS/paper.txt @ 3580

Last change on this file since 3580 was 3537, checked in by piccolo, 5 years ago

paper schema

File size: 3.7 KB
Line 
11) Sull'assembler:
2    - fattorizzare l'abstract interpretation in analisi dei basic block (analisi statica) /analisi dei flussi (dinamica)
3      NOTA: tenere conto che per associare staticamente un costo ai basic blocks un interprete astratto inferisce ed usa il
4           control flow;
5           un compilatore abs-interpretation aware trasferisce informazione quantitativa da sorgente a assmbler, noi non lo
6           facciamo, ma potremmo. Perchè pensiamo di essere meglio?
7    - assumiamo che ogni basic block inizi e termini con una label ed introduciamo una nozione di misurabile
8      (che tenga conto anche dell'input/output ovvero istruzioni che sfuggono all'interpretazione astratta poiche'
9       difficilmente predicibili o che introdurrebbero una approssimazione eccessiva)
10   - teorema statico dinamico
112) Fanta-compilatore:
12   assumere che il compilatore mandi i basic block nel sorgente in basic block nell'assembler ed inoltre che sia composizionale
13   in quanto la prima/ultima istruzione che emette l'etichetta si mapperebbe in un blocco la cui prima/ultima istruzione emetta
14   l'etichetta
15   Concludere che misurabile nel source implica misurabile nel target
16   Teorema: l'analisi statica del sorgente ovvero liftare l'analisi statica dell'assembler compilato nel sorgente per determinare
17   il costo delle etichette nel sorgente, ovvero teorema statico dinamico nel sorgente.
18   Capire come usarlo nell'instrumentazione (FRAMA C ?).
193) Compilatore più realistico -> assumere che il control flow venga preservato ma non la composizionalità
20  (un basic block nel sorgente viene mappato con le premesse e code silenti nell'assembler.
21  - Fare esempi: chiamate di funzione per passaggio di parametri, switch
22  - nuova definizione di misurabile e nuovo teorema di simulazione con code.
234) Chiamate di funzione/annidamento dei basic blocks
24   - monoide non abeliano -> non c'e' niente da fare, le chiamate sono tutte postlabelled
25   - monoide abeliano -> possibilità di effettuare una passata che trasforma le chiamate in chiamate post-labelled -> simulazione + statico dinamico
265) Classificazione passate
27   - preservano il control flow e le labels : simulation condition
28   - mancata preservazione del control flow: spiegare la soluzione di Paolo e come non impatti su tutte le altre passate (similarità/differenze con la prima passata post-labelled).
296) Formalizzazione.
30
31
32
33=================================================================================
341. problema generale: cost analysis at source level because...
352. problema specifico: indurre cost model sul sorgente
363. idea generale (labelling approach citato)
37   costo assembly = big_sum costo(basic block)
38   assunzione1: compilazione basic-block preserving
39     (citare lavoro sui loop)
40   assunzione2: costo basic blocks determinabile staticamente
41     (citare lavoro sull'hardware)
42   quindi: costo C = big_sum cost(basic block) = costo assembly
43
444. problemi
45   a) label emitting instructions:
46      una istruzione con due predecessori di cui uno if-then-else
47       compilabile solo come sequenza => impossibile da compilare
48
49      soluzione: gli archi determinano i costi e non i nodi
50
51   b) chiamate di funzione e linguaggi non strutturati
52
53      soluzione: tracce strutturate
54
55  [c) hardware: funzione di costo non commutativa => una label dopo ogni
56      chiamata; ma difficile ragionarci sopra nel caso di costo commutativo
57
58      soluzione: passata che mette le post-label
59  ]
60
615. sugo:
62
63   1. prova della passata che mette le post-label (work in progress, why
64      SOS is hard)
65
66   2. predicato di simulazione fra tracce strutturate + prova che tale
67      simulazione dimostra la preservazione dei costi
68
69   3. prova della statico-dinamica: vedi cerco, certificata dal fatto di usare
70      solo chiamate post-label
Note: See TracBrowser for help on using the repository browser.