== 
Labelling
=========

-- Labelling as a way to tackle the problem

Authors: 

Pro: Uncoupling of the cost computation from the labelling
     Abstract simulation via traces: no arithemtic; many cost models
     Cost computation by subsequent instrumentation
     Meta-programme of explicitation/reasons to believe 

Con: ACL2 (Piton) direct approach to problem via ``clock functions''
     Use LISP macros to translate clock functions to inductive reasoning

Future: consider space/stack height as a new cost model

Community: instead of lifting reasoning from AbsInt on object code back to source
           push reasoning back to the source level
           better than doing untrustworthy/but-trusted analysis via third party tools

Technical meaning of trust

-- Labelling applied to other languages/paradigms
   -- functional; done, but no gc, towards region-based gc
   -- laziness 
   -- oo; ???
   -- logic; maybe NOT: instrumentation/Hoare logic does not work for us (backtracking/failure)

Regions as a form of labelling derived from static analysis... 
... labelling derived for the ur static analysis: compiling

-- Dependent labelling

   Cost depends on label and status
   Simple abstractions support: 
     -- loop optimisation
     -- pipelines (dependency on status of the pipe)
   Cache analysis as future 

Authors: 

Pro: more fine-grained
     more realistic
     explicit, by comparison with black-box (AbsInt) methods
     better analysis of (loss of) precision
     actually: dependency is only on history (loop unrolling, pipelining)

Con: is it interesting?
     does it require us to have succeeded in publishing simple labelling first? 
     less automation than back-box methods 

A posteriori it should be! 

Future: -- primitives whose cost is state dependent (DIV)
	-- branch prediction (dependency on status of the machine) 
	-- *real* dependency on state 
	-- cache analysis


Community: abstract interpretation people

-- The "LUSTRE paper"...?

-- Ayache's Frama-C work?

== 
Formalisation
=============

-- Down to object code (VSTTE, FMCAD, ITP, CPP) 

Pro: beyond CompCert
     using dependent types
     optimising: branch displacement/code motion
     checking register allocation (sceptical checking)
     tried to split policy and implementation
     

Con: been done before
     who cares about dependent types? 
     what about sceptical checking of branch displacement policy? 
     failed to split policy and implementation

Proof of cost preservation: very complex, long time to get right
But: very much simplified after reflection; 
     a complex invariant (in ASM) is spread across two simpler ones (LINtoASM, LOAD); 
Stack overflow a problem in LINtoASM, not in LOAD
     
Future

Community

-- Branch displacement itself (Boender) 

Pro: self standing
Con: the ACL2 guys (again)!!!

Future

Community

-- The "structured traces" paper

The data structure
The cost preservation result itself
Bisimulation of structured traces implies equality of flattening

\Big\Sigma{l\in\flattentrace{\squareOmega} = clock \Delta

basic proof: rearranging (the sum over) a stuctured trace in to (the
sum over) a bracketed trace... "just" a permutation result

Pro: an intermediate between big- and small-step computation
     imposing a large-scale structure (for reasoning) on a small-step structure (for costing)
     "big" from label to label
     "small" between labels
     mixed-step approaches in Hoare logic? 
     semantics of "atomic(e)" in models of STM 

Con:

Future: 

Community: 


-- The overall formalisation as a paper

Pro: what, and how
     the unified language
     software engineering with dependent types 

Con: what, and why is it interesting? 
     will it be accepted anywhere?

Future: ?

Community: journals JAR, AFP; maybe CPP, ITP...

-- A high-level survey paper (SP&E?)

Pro: what, and how
     software engineering with dependent types 

Con: what, and why is it interesting? 
     will it be accepted anywhere?

Future: ?

Community: journals: SP&E?