Changeset 3537

Timestamp:

Mar 16, 2015, 5:45:44 PM (6 years ago)

Author:

piccolo

Message:

paper schema

File:

• LTS/paper.txt (modified) (1 diff)

LTS/paper.txt

@@ +1 @@
+1) Sull'assembler:
+    - fattorizzare l'abstract interpretation in analisi dei basic block (analisi statica) /analisi dei flussi (dinamica)
+      NOTA: tenere conto che per associare staticamente un costo ai basic blocks un interprete astratto inferisce ed usa il
+           control flow;
+           un compilatore abs-interpretation aware trasferisce informazione quantitativa da sorgente a assmbler, noi non lo 
+           facciamo, ma potremmo. Perchè pensiamo di essere meglio?
+    - assumiamo che ogni basic block inizi e termini con una label ed introduciamo una nozione di misurabile 
+      (che tenga conto anche dell'input/output ovvero istruzioni che sfuggono all'interpretazione astratta poiche' 
+       difficilmente predicibili o che introdurrebbero una approssimazione eccessiva)
+   - teorema statico dinamico
+2) Fanta-compilatore:
+   assumere che il compilatore mandi i basic block nel sorgente in basic block nell'assembler ed inoltre che sia composizionale
+   in quanto la prima/ultima istruzione che emette l'etichetta si mapperebbe in un blocco la cui prima/ultima istruzione emetta
+   l'etichetta
+   Concludere che misurabile nel source implica misurabile nel target
+   Teorema: l'analisi statica del sorgente ovvero liftare l'analisi statica dell'assembler compilato nel sorgente per determinare
+   il costo delle etichette nel sorgente, ovvero teorema statico dinamico nel sorgente.
+   Capire come usarlo nell'instrumentazione (FRAMA C ?).
+3) Compilatore più realistico -> assumere che il control flow venga preservato ma non la composizionalità
+  (un basic block nel sorgente viene mappato con le premesse e code silenti nell'assembler.
+  - Fare esempi: chiamate di funzione per passaggio di parametri, switch
+  - nuova definizione di misurabile e nuovo teorema di simulazione con code.
+4) Chiamate di funzione/annidamento dei basic blocks
+   - monoide non abeliano -> non c'e' niente da fare, le chiamate sono tutte postlabelled
+   - monoide abeliano -> possibilità di effettuare una passata che trasforma le chiamate in chiamate post-labelled -> simulazione + statico dinamico
+5) Classificazione passate 
+   - preservano il control flow e le labels : simulation condition
+   - 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).
+6) Formalizzazione.
+
+
+
+=================================================================================
 1. problema generale: cost analysis at source level because...
 2. problema specifico: indurre cost model sul sorgente