source: Deliverables/D6.2/publist-notes.txt @ 1990

Last change on this file since 1990 was 1990, checked in by mckinna, 8 years ago

the LUSTRE paper has not yet appeared
what about the Ayache/Frama?-C paper(s)?

File size: 3.9 KB
Line 
1==
2Labelling
3=========
4
5-- Labelling as a way to tackle the problem
6
7Authors:
8
9Pro: Uncoupling of the cost computation from the labelling
10     Abstract simulation via traces: no arithemtic; many cost models
11     Cost computation by subsequent instrumentation
12     Meta-programme of explicitation/reasons to believe
13
14Con: ACL2 (Piton) direct approach to problem via ``clock functions''
15     Use LISP macros to translate clock functions to inductive reasoning
16
17Future: consider space/stack height as a new cost model
18
19Community: instead of lifting reasoning from AbsInt on object code back to source
20           push reasoning back to the source level
21           better than doing untrustworthy/but-trusted analysis via third party tools
22
23Technical meaning of trust
24
25-- Labelling applied to other languages/paradigms
26   -- functional; done, but no gc, towards region-based gc
27   -- laziness
28   -- oo; ???
29   -- logic; maybe NOT: instrumentation/Hoare logic does not work for us (backtracking/failure)
30
31Regions as a form of labelling derived from static analysis...
32... labelling derived for the ur static analysis: compiling
33
34-- Dependent labelling
35
36   Cost depends on label and status
37   Simple abstractions support:
38     -- loop optimisation
39     -- pipelines (dependency on status of the pipe)
40   Cache analysis as future
41
42Authors:
43
44Pro: more fine-grained
45     more realistic
46     explicit, by comparison with black-box (AbsInt) methods
47     better analysis of (loss of) precision
48     actually: dependency is only on history (loop unrolling, pipelining)
49
50Con: is it interesting?
51     does it require us to have succeeded in publishing simple labelling first?
52     less automation than back-box methods
53
54A posteriori it should be!
55
56Future: -- primitives whose cost is state dependent (DIV)
57        -- branch prediction (dependency on status of the machine)
58        -- *real* dependency on state
59        -- cache analysis
60
61
62Community: abstract interpretation people
63
64-- The "LUSTRE paper"...
65
66==
67Formalisation
68=============
69
70-- Down to object code (VSTTE, FMCAD, ITP, CPP)
71
72Pro: beyond CompCert
73     using dependent types
74     optimising: branch displacement/code motion
75     checking register allocation (sceptical checking)
76     tried to split policy and implementation
77     
78
79Con: been done before
80     who cares about dependent types?
81     what about sceptical checking of branch displacement policy?
82     failed to split policy and implementation
83
84Proof of cost preservation: very complex, long time to get right
85But: very much simplified after reflection;
86     a complex invariant (in ASM) is spread across two simpler ones (LINtoASM, LOAD);
87Stack overflow a problem in LINtoASM, not in LOAD
88     
89Future
90
91Community
92
93-- Branch displacement itself (Boender)
94
95Pro: self standing
96Con: the ACL2 guys (again)!!!
97
98Future
99
100Community
101
102-- The "structured traces" paper
103
104The data structure
105The cost preservation result itself
106Bisimulation of structured traces implies equality of flattening
107
108\Big\Sigma{l\in\flattentrace{\squareOmega} = clock \Delta
109
110basic proof: rearranging (the sum over) a stuctured trace in to (the
111sum over) a bracketed trace... "just" a permutation result
112
113Pro: an intermediate between big- and small-step computation
114     imposing a large-scale structure (for reasoning) on a small-step structure (for costing)
115     "big" from label to label
116     "small" between labels
117     mixed-step approaches in Hoare logic?
118     semantics of "atomic(e)" in models of STM
119
120Con:
121
122Future:
123
124Community:
125
126
127-- The overall formalisation as a paper
128
129Pro: what, and how
130     the unified language
131     software engineering with dependent types
132
133Con: what, and why is it interesting?
134     will it be accepted anywhere?
135
136Future: ?
137
138Community: journals JAR, AFP; maybe CPP, ITP...
139
140-- A high-level survey paper (SP&E?)
141
142Pro: what, and how
143     software engineering with dependent types
144
145Con: what, and why is it interesting?
146     will it be accepted anywhere?
147
148Future: ?
149
150Community: journals: SP&E?
151
152
153
Note: See TracBrowser for help on using the repository browser.