1. problema generale: cost analysis at source level because... 2. problema specifico: indurre cost model sul sorgente 3. idea generale (labelling approach citato) costo assembly = big_sum costo(basic block) assunzione1: compilazione basic-block preserving (citare lavoro sui loop) assunzione2: costo basic blocks determinabile staticamente (citare lavoro sull'hardware) quindi: costo C = big_sum cost(basic block) = costo assembly 4. problemi a) label emitting instructions: una istruzione con due predecessori di cui uno if-then-else compilabile solo come sequenza => impossibile da compilare soluzione: gli archi determinano i costi e non i nodi b) chiamate di funzione e linguaggi non strutturati soluzione: tracce strutturate [c) hardware: funzione di costo non commutativa => una label dopo ogni chiamata; ma difficile ragionarci sopra nel caso di costo commutativo soluzione: passata che mette le post-label ] 5. sugo: 1. prova della passata che mette le post-label (work in progress, why SOS is hard) 2. predicato di simulazione fra tracce strutturate + prova che tale simulazione dimostra la preservazione dei costi 3. prova della statico-dinamica: vedi cerco, certificata dal fatto di usare solo chiamate post-label