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

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

Ayache?

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-- Ayache's Frama-C work?
67
68==
69Formalisation
70=============
71
72-- Down to object code (VSTTE, FMCAD, ITP, CPP)
73
74Pro: beyond CompCert
75     using dependent types
76     optimising: branch displacement/code motion
77     checking register allocation (sceptical checking)
78     tried to split policy and implementation
79     
80
81Con: been done before
82     who cares about dependent types?
83     what about sceptical checking of branch displacement policy?
84     failed to split policy and implementation
85
86Proof of cost preservation: very complex, long time to get right
87But: very much simplified after reflection;
88     a complex invariant (in ASM) is spread across two simpler ones (LINtoASM, LOAD);
89Stack overflow a problem in LINtoASM, not in LOAD
90     
91Future
92
93Community
94
95-- Branch displacement itself (Boender)
96
97Pro: self standing
98Con: the ACL2 guys (again)!!!
99
100Future
101
102Community
103
104-- The "structured traces" paper
105
106The data structure
107The cost preservation result itself
108Bisimulation of structured traces implies equality of flattening
109
110\Big\Sigma{l\in\flattentrace{\squareOmega} = clock \Delta
111
112basic proof: rearranging (the sum over) a stuctured trace in to (the
113sum over) a bracketed trace... "just" a permutation result
114
115Pro: an intermediate between big- and small-step computation
116     imposing a large-scale structure (for reasoning) on a small-step structure (for costing)
117     "big" from label to label
118     "small" between labels
119     mixed-step approaches in Hoare logic?
120     semantics of "atomic(e)" in models of STM
121
122Con:
123
124Future:
125
126Community:
127
128
129-- The overall formalisation as a paper
130
131Pro: what, and how
132     the unified language
133     software engineering with dependent types
134
135Con: what, and why is it interesting?
136     will it be accepted anywhere?
137
138Future: ?
139
140Community: journals JAR, AFP; maybe CPP, ITP...
141
142-- A high-level survey paper (SP&E?)
143
144Pro: what, and how
145     software engineering with dependent types
146
147Con: what, and why is it interesting?
148     will it be accepted anywhere?
149
150Future: ?
151
152Community: journals: SP&E?
153
154
155
Note: See TracBrowser for help on using the repository browser.