Timeline



Sep 28, 2011:

11:50 PM Changeset [1282] by sacerdot
Cosmetic change: names of joint statements/instructions shortened and …
11:08 PM Changeset [1281] by sacerdot
Porting of all transformation to the joint syntax practically …
2:43 AM Changeset [1280] by sacerdot
Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) …
2:41 AM Changeset [1279] by sacerdot
Bug fixed in definition of ltb.

Sep 27, 2011:

9:57 AM Changeset [1278] by sacerdot
oppargs requires two more arguments. RTLtoERTL to be fixed since it …

Sep 26, 2011:

6:58 PM Changeset [1277] by campbell
Runtime functions and conclusion for D3.2.
6:14 PM Changeset [1276] by campbell
Support for replacing operations with runtime support functions in …
6:07 PM Changeset [1275] by sacerdot
RTL ported to joint syntax, but: 1. bug discovered: opaccs should …
5:58 PM Changeset [1274] by mulligan
starting removing axioms from adts and giving them proper implementations
5:57 PM Changeset [1273] by campbell
Remove generated file.
5:57 PM Changeset [1272] by campbell
Revert accidental commit.
4:24 PM Changeset [1271] by mulligan
finished, kind of
3:59 PM Changeset [1270] by sacerdot
Making RTL syntax an instance of Joint.
3:06 PM Changeset [1269] by sacerdot
Useless include removed.
2:52 PM Changeset [1268] by sacerdot
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
12:41 PM Changeset [1267] by campbell
Other bits and pieces for D3.3.
12:09 PM Changeset [1266] by sacerdot
Added second projection.
11:29 AM Changeset [1265] by campbell
Revisions to D3.3.

Sep 23, 2011:

6:44 PM Changeset [1264] by sacerdot
Almost ported to new Joint syntax.
5:12 PM Changeset [1263] by mulligan
changes
4:40 PM Changeset [1262] by sacerdot
RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …
4:17 PM Changeset [1261] by campbell
More of D3.2.
3:04 PM Changeset [1260] by mulligan
commit for csc
11:49 AM Changeset [1259] by sacerdot
More progress towards new Joint data type.
1:47 AM Changeset [1258] by sacerdot
More progress towards porting to joint syntax.

Sep 22, 2011:

6:04 PM Changeset [1257] by sacerdot
More progress in porting to joint datatype.
6:03 PM Changeset [1256] by mulligan
changes: added a mapi for graphs
4:23 PM Changeset [1255] by sacerdot
Major mistake fixed: op1 and op2 were assuming the source and dest …
4:16 PM Changeset [1254] by sacerdot
More progress towards porting of RTLtoERTL to joint syntax.
2:57 PM Changeset [1253] by mulligan
uses.ma finished
2:49 PM Changeset [1252] by sacerdot
graph_params added to joint/Joint.ma, together with useful common …
2:29 PM Changeset [1251] by mulligan
changes to get things compiling again after yet another CSC rearrangement!
12:02 PM Changeset [1250] by sacerdot
1. Sigma types projections moved to utilities/extralib.ma 2. Extended …
11:41 AM Changeset [1249] by mulligan
changes to get everything to typecheck again
10:13 AM Changeset [1248] by mulligan
deleted files that do not compile in utilities, changed ertl.ma to use …
3:03 AM Changeset [1247] by sacerdot
Code (almost) ported to latest joint/Joint.ma datatype. I still need …
2:50 AM Changeset [1246] by sacerdot
Yet another change to Joint.ma to accomodate all passes. The concrete …

Sep 21, 2011:

10:22 PM Changeset [1245] by sacerdot
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
6:08 PM Changeset [1244] by campbell
Sort out Clight semantics equivalence proof for new SmallstepExec?.
5:53 PM Changeset [1243] by mulligan
small changes
5:35 PM Changeset [1242] by sacerdot
Some clean-up.
5:28 PM Changeset [1241] by mulligan
changes for claudio
5:24 PM Changeset [1240] by sacerdot
Ported to common definitions.
5:21 PM Changeset [1239] by sacerdot
RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is …
4:25 PM Changeset [1238] by campbell
Update Cminor and RTLabs to fit SmallstepExec? changes.
3:58 PM Changeset [1237] by sacerdot
Wrong commit repaired.
3:56 PM Changeset [1236] by sacerdot
LTLToLin.ma completed (up to a couple of daemons used to provide dead …
12:14 PM Changeset [1235] by campbell
Some basic material for D3.2, but not yet finished.
12:14 PM Changeset [1234] by campbell
Add (rather brief) draft of D3.3.
11:57 AM Changeset [1233] by sacerdot
1) Ported to Brian's new dependent type for fullexec 2) Universe level …
11:24 AM Changeset [1232] by mulligan
big changes: got what was implemented in the ertl to ltl pass type …

Sep 20, 2011:

7:11 PM Changeset [1231] by campbell
Change SmallstepExec? so that states can depend on global information. …
3:56 PM Changeset [1230] by mulligan
more changes
1:26 PM Changeset [1229] by mulligan
changes

Sep 19, 2011:

4:52 PM Changeset [1228] by mulligan
some more changes
12:57 PM Changeset [1227] by mulligan
changes

Sep 16, 2011:

7:16 PM Changeset [1226] by campbell
Adjust pretty printers for change in program records, try a test of each.
6:48 PM Changeset [1225] by campbell
Missing ; in proof
6:39 PM Changeset [1224] by sacerdot
Type of programs in common/AST made more dependent. In particular, the …
5:15 PM Changeset [1223] by mulligan
changes
11:02 AM Changeset [1222] by sacerdot
LTL fully ported to the joint syntax.
10:53 AM Changeset [1221] by sacerdot
Cleanup.

Sep 15, 2011:

6:05 PM Changeset [1220] by sacerdot
ERTL ported to the new joint syntax.
5:40 PM Changeset [1219] by mulligan
a little more added
4:56 PM Changeset [1218] by mulligan
a lot added to interference graph calculation
4:42 PM Changeset [1217] by sacerdot
Only one axiom left.
3:33 PM Changeset [1216] by campbell
Update Clight semantics equivalence proof to match changes in …
3:04 PM Changeset [1215] by sacerdot
1) Added shifting directly on pointers 2) More temporary axioms closed.
2:27 PM Changeset [1214] by sacerdot
res_to_opt function added to common/Errors and used in joint/semantics …
2:01 PM Changeset [1213] by sacerdot
1) New values (joint/BEValues.ma) and memory model for the back-ends …

Sep 14, 2011:

5:03 PM Changeset [1212] by mulligan
more added on interference graphs
4:14 PM Changeset [1211] by mulligan
fixed interference file
4:04 PM Changeset [1210] by mulligan
getting rid of typeclass-like records in favour of file-level axioms. …

Sep 13, 2011:

5:14 PM Changeset [1209] by mulligan
more work on int. graphs
4:33 PM Changeset [1208] by mulligan
added adts for sets, tables and priority sets in order to make life …

Sep 12, 2011:

4:20 PM Changeset [1207] by campbell
Second part of fixing temporaries in Clight to Cminor stage.
4:20 PM Changeset [1206] by campbell
First stage of fixing temporary generation in Clight/toCminor.ma.

Sep 10, 2011:

12:16 PM Changeset [1205] by mulligan
typographical changes
12:13 PM Changeset [1204] by mulligan
small change
12:09 PM Changeset [1203] by mulligan
implemented referees comments

Sep 9, 2011:

11:48 AM Changeset [1202] by mulligan
more changes, changed mention of atkey's jvm
11:27 AM Changeset [1201] by mulligan
more changes to reduce length
11:03 AM Changeset [1200] by mulligan
small changes and rewordings to decrease length
9:49 AM Changeset [1199] by mulligan
got paper down to 15 and a half pages with nothing much added to document

Sep 8, 2011:

4:04 PM Changeset [1198] by campbell
Clight cast removal (NB: quite different from the prototype).

Sep 7, 2011:

12:10 PM Changeset [1197] by campbell
Merge trunk to branch.

Sep 6, 2011:

6:15 PM Changeset [1196] by mulligan
some more changes, need some additional datastructures
5:20 PM Changeset [1195] by campbell
List find function.
5:20 PM Changeset [1194] by campbell
Remove old, commented out code.
3:49 PM Changeset [1193] by mulligan
work on colouring algorithm halted as it can be axiomatised. now …
1:33 PM Changeset [1192] by mulligan
some files that were missing / laying dormant on my computer
10:38 AM Changeset [1191] by mulligan
ertl to ertl pass back where it was before the changes to joint

Sep 5, 2011:

5:53 PM Changeset [1190] by mulligan
improved explanation of matita
5:23 PM Changeset [1189] by mulligan
implemented some language fixes as spotted by the referees
5:14 PM Changeset [1188] by mulligan
removed stray lines from uses.ma so that it at least typechecks
5:13 PM Changeset [1187] by mulligan
fixed build.ma
5:08 PM Changeset [1186] by sacerdot
Spurious code removed. joint_fullexec implemented up to …
5:02 PM Changeset [1185] by mulligan
ported liveness analysis to new code
2:55 PM Changeset [1184] by mulligan
changed to llncs style and increased font size in code extracts
1:31 PM Changeset [1183] by mulligan
removed parameterised label types in the three lowest level languages
1:23 PM Changeset [1182] by mulligan
changes to semantics: removing parameterised "next" element in joint …
1:11 PM Changeset [1181] by mulligan
changed smallstep exec in order to remove matita bug (superposition.ml …
12:01 PM Changeset [1180] by mulligan
lin to ltl pass complete
11:58 AM Changeset [1179] by mulligan
changes to ertl, ltl and lin to use new notion of joint params. ertl …
11:26 AM Changeset [1178] by mulligan
fixed ertl.ma to use new version of joint params

Sep 4, 2011:

9:36 PM Changeset [1177] by sacerdot
Almost finished. Some functions still to be implemented, but I suspect …

Sep 3, 2011:

4:17 AM Changeset [1176] by sacerdot

Sep 2, 2011:

5:58 PM Changeset [1175] by mulligan
changes to ertl pass
4:09 PM Changeset [1174] by sacerdot
Semantics of most instructions completed.
3:33 PM Changeset [1173] by sacerdot
Unified semantics for ERTL/LTL/LIN (in progress). I hope to include …
3:00 PM Changeset [1172] by mulligan
ertltoltl.ma half complete
2:51 PM Changeset [1171] by mulligan
changes made on claudio's request: changed order of nesting in the …
12:28 PM Changeset [1170] by mulligan
changes to ertl > ltl pass
11:57 AM Changeset [1169] by sacerdot
JointRTLtoLIN moved to Joint
11:36 AM Changeset [1168] by sacerdot
Joint statements parameterized over a record.
10:35 AM Changeset [1167] by mulligan
10:35 AM Changeset [1166] by mulligan
moved joint ltl lin files into their own directory. more changes to …

Sep 1, 2011:

5:18 PM Changeset [1165] by mulligan
more changes
4:53 PM Changeset [1164] by mulligan
ltl to lin working again, more changes to joint syntax
4:23 PM Changeset [1163] by mulligan
even more streamlining and fixes to get things type checking
11:32 AM Changeset [1162] by mulligan
changes committed to ertl semantics based on our new combined syntax …

Aug 31, 2011:

6:24 PM Changeset [1161] by mulligan
changes from today: merged ertl, ltl and lin into one datatype to …
12:30 PM Changeset [1160] by mulligan
changes to unfunctorised code in ertltoltl.ma
12:30 PM Changeset [1159] by boender
- added 'nth' theorems - moved up \bot a bit
12:15 PM Changeset [1158] by campbell
Record patch needed to use matita pretty printers with acc.
12:15 PM Changeset [1157] by campbell
Update pretty printers and examples.
11:41 AM Changeset [1156] by sacerdot
ERTL semantics completed up to initialization and memory model.
11:26 AM Changeset [1155] by mulligan
removed
11:26 AM Changeset [1154] by mulligan
changes to ertl files: in process of removing ertltoltli.ma in favour …

Aug 30, 2011:

6:55 PM Changeset [1153] by campbell
Merge trunk into branch.
5:43 PM Changeset [1152] by mulligan
more added
4:56 PM Changeset [1151] by sacerdot
Only new_/del_frame and framesize left.
4:23 PM Changeset [1150] by sacerdot
Push/pop implemented.
4:22 PM Changeset [1149] by mulligan
changes to get everything type checking again after changing names of …
4:14 PM Changeset [1148] by sacerdot
Function call/return finished (up to retrieving parameters from the …
4:09 PM Changeset [1147] by campbell
Remove some obsolete commented out code, update a couple of comments.
4:07 PM Changeset [1146] by sacerdot
More progress: function call/return almost completed.
4:02 PM Changeset [1145] by mulligan
changed naming in i8051 of classes of registers to make them consistent
3:53 PM Changeset [1144] by mulligan
added build.ma file. matita bug found
3:39 PM Changeset [1143] by sacerdot
Added one important observation (not implemented yet).
3:33 PM Changeset [1142] by sacerdot
More progress.
3:33 PM Changeset [1141] by sacerdot
Comment (about a bug) added.
2:23 PM Changeset [1140] by sacerdot
More instructions implemented.
12:47 PM Changeset [1139] by campbell
Shift init_data out of generic program record so that it only appears …
12:08 PM Changeset [1138] by mulligan
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other

Aug 29, 2011:

6:27 PM Changeset [1137] by sacerdot
More progress.
6:01 PM Changeset [1136] by mulligan
fixed ertl pass
5:45 PM Changeset [1135] by campbell
Add invariants to Cminor semantics to rule out some failures.
5:45 PM Changeset [1134] by campbell
Extra results for non-failing map updates.
5:45 PM Changeset [1133] by campbell
Add missing utilities files
5:30 PM Changeset [1132] by mulligan
reunified ltl and lin instruction type, removing lifting in ltl and …
5:19 PM Changeset [1131] by mulligan
changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h …
5:11 PM Changeset [1130] by sacerdot
File in progress (copied from RTL). All instructions considered up to …
4:34 PM Changeset [1129] by mulligan
removed conversions between Register and register
4:27 PM Changeset [1128] by mulligan
fixed ERTLtoLTLI so it type checks again
3:30 PM Changeset [1127] by mulligan
interference graphs axiomatised, more added to ertl
3:07 PM Changeset [1126] by sacerdot
Semantics completed up to initial state creation.
3:07 PM Changeset [1125] by sacerdot
Monadic mfold_left2 added.
2:42 PM Changeset [1124] by mulligan
finished off liveness analysis by axiomatising properties
2:34 PM Changeset [1123] by sacerdot
Added comment about missing alignment of data in memory.
Note: See TracTimeline for information about the timeline view.