Timeline



Dec 21, 2012:

4:44 PM HiPEAC13 edited by campbell
(diff)
4:42 PM HiPEAC13 edited by campbell
(diff)
4:41 PM HiPEAC13 edited by campbell
(diff)
4:36 PM HiPEAC13 edited by campbell
(diff)

Dec 19, 2012:

6:55 PM Changeset [2566] by piccolo
ERTL to ERTLptr pass implemented up to a few things to be left to the …
6:11 PM Changeset [2565] by garnier
Cl to Cm progress.
12:46 PM Changeset [2564] by piccolo
ERTL fully repaired, useless part of return value of pop_ra removed.
11:58 AM Changeset [2563] by piccolo
Repairing ERTL: show stopper found.
10:38 AM Changeset [2562] by piccolo
linearise modified

Dec 18, 2012:

5:03 PM Changeset [2561] by tranquil
* moved CALL as different case than joint_seq: lots of broken code now …
4:38 PM Changeset [2560] by garnier
Fix in trace gen for CL
1:56 PM Changeset [2559] by piccolo
lineariseProof finished
8:40 AM Changeset [2558] by amadio
r

Dec 17, 2012:

2:35 PM Changeset [2557] by tranquil
minor modification of commented (for now) proof of correctness of …

Dec 14, 2012:

2:54 PM Changeset [2556] by tranquil
in joint semantics and traces: added a last popped calling address to …
12:40 AM Changeset [2555] by piccolo
lemma eval_call_ok finished

Dec 13, 2012:

5:22 PM Changeset [2554] by garnier
Proof of expression translation correctness "mostly" done for CL to …

Dec 12, 2012:

2:43 PM Changeset [2553] by tranquil
as_classify changed to a partial function added a status for tailcalls

Dec 11, 2012:

3:19 PM Changeset [2552] by mulligan
Some different ideas, don't seem to be working out well.
2:17 AM HiPEAC13 edited by campbell
(diff)

Dec 10, 2012:

8:11 PM Changeset [2551] by piccolo
completed isFinal and fetchStatementSigmaCommute. Fixed exit …
6:39 PM Changeset [2550] by mulligan
Some new ideas that lead to non-termination…
4:44 PM Changeset [2549] by mulligan
Not as straightforward as first imagined…
2:33 PM Changeset [2548] by tranquil
in BackEndOps?, cleaner def of be_op2 new statement of …

Dec 7, 2012:

8:37 PM Changeset [2547] by tranquil
going on in proof of linearise simplified by use of monadic functional …
6:49 PM Changeset [2546] by mulligan
Some more progress.
6:39 PM Changeset [2545] by garnier
Comitting current progress of CL to CM
5:52 PM Changeset [2544] by mulligan
More added, painful crash course in learning Agda. Seem to have the …
11:35 AM Changeset [2543] by piccolo
finished stmt_at_sigma_commute
11:13 AM Changeset [2542] by mulligan
Trying an Agda port of the polymorphic variants implementation to see …

Dec 6, 2012:

4:02 PM Changeset [2541] by tranquil
adapted size notation to last matita lib update (01/12/2012) that …
3:17 PM Changeset [2540] by tranquil
cl_jump case now provides a proof of costedness of the following state
2:48 PM Changeset [2539] by tranquil
added cl_jump case to trace_any_any_free
1:39 PM Changeset [2538] by tranquil
fixed Traces.ma after changes in joint/semantics.ma
1:24 PM Changeset [2537] by tranquil
rolled back changes on calls in joint. Now the save_frame parameter …
1:18 PM Changeset [2536] by piccolo
finished eval_seq_no_pc_sigma_commute lemma

Dec 5, 2012:

7:20 PM Changeset [2535] by campbell
Add the trivial C program with check that there's a measurable subtrace.
7:20 PM Changeset [2534] by campbell
Tweak measurable definition to stop at the return from a function.
7:20 PM Changeset [2533] by campbell
Some fall out from removing floats.
6:57 PM Changeset [2532] by tranquil
added FCOND in LIN, and rewritten linearise so that it never adds a …
1:28 PM Changeset [2531] by mckinna
Trivial tweaks.

Dec 4, 2012:

6:29 PM Changeset [2530] by tranquil
temporary switch to cl_jump treated as cl_other fixed script for new …
6:16 PM Changeset [2529] by tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
9:05 AM Changeset [2528] by piccolo
added cases PUSH, C_ADDRESS and COPACCS

Dec 3, 2012:

6:22 PM Changeset [2527] by garnier
Progress on CL to CM.
5:48 PM Changeset [2526] by sacerdot
5:39 PM Changeset [2525] by sacerdot
4:41 PM Changeset [2524] by mulligan
Avoiding conflicts
4:30 PM Changeset [2523] by sacerdot
4:15 PM Changeset [2522] by sacerdot
Generic stuff moved to infrastructure.
4:10 PM Changeset [2521] by sacerdot
..
4:07 PM Changeset [2520] by sacerdot
Now it is nice!
12:29 PM Changeset [2519] by mulligan
To prevent conflicts
12:28 PM Changeset [2518] by sacerdot
11:51 AM Changeset [2517] by sacerdot

Dec 2, 2012:

5:45 PM Changeset [2516] by mckinna
removed typedefs; restored older versions; moved typedefs to …
5:20 PM Changeset [2515] by sacerdot
4:40 PM Changeset [2514] by sacerdot
All .ma files committed: some of them are just in-progress.

Dec 1, 2012:

9:01 PM Changeset [2513] by mckinna
Minor tweaks. Simplified dependencies again.
8:36 PM Changeset [2512] by mckinna
Simplified dependencies on ASM, to allow rollback to when …

Nov 30, 2012:

6:31 PM Changeset [2511] by campbell
Conjecture main Cminor/RTLabs simulation results. Add a few notes …
4:40 PM Changeset [2510] by garnier
Some progress on the Cl -> Cm front
1:15 PM Changeset [2509] by campbell
misc note

Nov 29, 2012:

8:12 PM Changeset [2508] by mckinna
more tweaks. compiler and correctness still build.
7:14 PM Changeset [2507] by piccolo
finished pop case in commutation eval_Seq_no_pc
6:38 PM Changeset [2506] by campbell
Use common definition of measurable.
3:37 PM Changeset [2505] by mckinna
Cleaned up compiler.ma; some refactoring/additional code needed in …
3:33 PM Changeset [2504] by mckinna
More refactoring to support the tidied up compiler.ma
3:32 PM Changeset [2503] by mckinna
tidied up, with new auxiliary defns, some refactoring, some code …
11:59 AM Changeset [2502] by campbell
Sketch a little about how measurable traces might work with RTLabs and …
10:12 AM Changeset [2501] by piccolo
working on lineariseProof. Not yet finished.

Nov 28, 2012:

5:57 PM Changeset [2500] by garnier
Continuing work on simulation in Clight/Cminor?
12:52 PM Changeset [2499] by campbell
Separate out the RTLabs abstract status record from the proofs about …

Nov 27, 2012:

6:01 PM Changeset [2498] by mckinna
Refactor: Typedefs object_code and costlabel_map lifted out from …
5:59 PM Changeset [2497] by mckinna
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
5:50 PM Changeset [2496] by garnier
Some tentative work on the simulation proof for expressions, in order …
5:17 PM Changeset [2495] by piccolo
continuing lineariseProof

Nov 26, 2012:

6:24 PM Changeset [2494] by mckinna
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
6:00 PM Changeset [2493] by mckinna
Change in cst_well_defd to fix previously broken defn of …
11:52 AM Changeset [2492] by campbell
Reduce axiomatisation in compiler.ma.
11:30 AM Changeset [2491] by tranquil
fixed wrt change of list member definition

Nov 25, 2012:

1:33 PM Changeset [2490] by tranquil
switched back to Byte immediate (instead of beval ones) propagated …

Nov 23, 2012:

5:28 PM Changeset [2489] by campbell
Conjecture some Clight/Cminor? simulation results.
4:29 PM Changeset [2488] by garnier
glitch fixed
3:47 PM Changeset [2487] by campbell
Set up "after_n_steps" to enforce an invariant on states.
12:18 PM Changeset [2486] by campbell
First go at a generalised version of measurable.
11:22 AM Changeset [2485] by campbell
Sketch of Clight/Cminor? callstate simulation

Nov 22, 2012:

6:40 PM Changeset [2484] by piccolo
fixed Traces and semantics added commutation record (not yet finished) …
5:05 PM Changeset [2483] by garnier
Memory injections for Clight to Cminor, partially axiomatized.
3:49 PM Changeset [2482] by campbell
Note about front-end simulations
10:09 AM HiPEAC13 edited by amadio
(diff)

Nov 21, 2012:

12:12 PM HiPEAC13 created by campbell
Note: See TracTimeline for information about the timeline view.