Timeline
Dec 21, 2012:
- 4:44 PM HiPEAC13 edited by
- (diff)
- 4:42 PM HiPEAC13 edited by
- (diff)
- 4:41 PM HiPEAC13 edited by
- (diff)
- 4:36 PM HiPEAC13 edited by
- (diff)
Dec 19, 2012:
- 6:55 PM Changeset [2566] by
- ERTL to ERTLptr pass implemented up to a few things to be left to the …
- 6:11 PM Changeset [2565] by
- Cl to Cm progress.
- 12:46 PM Changeset [2564] by
- ERTL fully repaired, useless part of return value of pop_ra removed.
- 11:58 AM Changeset [2563] by
- Repairing ERTL: show stopper found.
- 10:38 AM Changeset [2562] by
- linearise modified
Dec 18, 2012:
- 5:03 PM Changeset [2561] by
- * moved CALL as different case than joint_seq: lots of broken code now …
- 4:38 PM Changeset [2560] by
- Fix in trace gen for CL
- 1:56 PM Changeset [2559] by
- lineariseProof finished
- 8:40 AM Changeset [2558] by
- r
Dec 17, 2012:
- 2:35 PM Changeset [2557] by
- minor modification of commented (for now) proof of correctness of …
Dec 14, 2012:
- 2:54 PM Changeset [2556] by
- in joint semantics and traces: added a last popped calling address to …
- 12:40 AM Changeset [2555] by
- lemma eval_call_ok finished
Dec 13, 2012:
- 5:22 PM Changeset [2554] by
- Proof of expression translation correctness "mostly" done for CL to …
Dec 12, 2012:
- 2:43 PM Changeset [2553] by
- as_classify changed to a partial function added a status for tailcalls
Dec 11, 2012:
- 3:19 PM Changeset [2552] by
- Some different ideas, don't seem to be working out well.
- 2:17 AM HiPEAC13 edited by
- (diff)
Dec 10, 2012:
- 8:11 PM Changeset [2551] by
- completed isFinal and fetchStatementSigmaCommute. Fixed exit …
- 6:39 PM Changeset [2550] by
- Some new ideas that lead to non-termination…
- 4:44 PM Changeset [2549] by
- Not as straightforward as first imagined…
- 2:33 PM Changeset [2548] by
- in BackEndOps?, cleaner def of be_op2 new statement of …
Dec 7, 2012:
- 8:37 PM Changeset [2547] by
- going on in proof of linearise simplified by use of monadic functional …
- 6:49 PM Changeset [2546] by
- Some more progress.
- 6:39 PM Changeset [2545] by
- Comitting current progress of CL to CM
- 5:52 PM Changeset [2544] by
- More added, painful crash course in learning Agda. Seem to have the …
- 11:35 AM Changeset [2543] by
- finished stmt_at_sigma_commute
- 11:13 AM Changeset [2542] by
- Trying an Agda port of the polymorphic variants implementation to see …
Dec 6, 2012:
- 4:02 PM Changeset [2541] by
- adapted size notation to last matita lib update (01/12/2012) that …
- 3:17 PM Changeset [2540] by
- cl_jump case now provides a proof of costedness of the following state
- 2:48 PM Changeset [2539] by
- added cl_jump case to trace_any_any_free
- 1:39 PM Changeset [2538] by
- fixed Traces.ma after changes in joint/semantics.ma
- 1:24 PM Changeset [2537] by
- rolled back changes on calls in joint. Now the save_frame parameter …
- 1:18 PM Changeset [2536] by
- finished eval_seq_no_pc_sigma_commute lemma
Dec 5, 2012:
- 7:20 PM Changeset [2535] by
- Add the trivial C program with check that there's a measurable subtrace.
- 7:20 PM Changeset [2534] by
- Tweak measurable definition to stop at the return from a function.
- 7:20 PM Changeset [2533] by
- Some fall out from removing floats.
- 6:57 PM Changeset [2532] by
- added FCOND in LIN, and rewritten linearise so that it never adds a …
- 1:28 PM Changeset [2531] by
- Trivial tweaks.
Dec 4, 2012:
- 6:29 PM Changeset [2530] by
- temporary switch to cl_jump treated as cl_other fixed script for new …
- 6:16 PM Changeset [2529] by
- rewritten function handling in joint swapped call_rel with ret_rel in …
- 9:05 AM Changeset [2528] by
- added cases PUSH, C_ADDRESS and COPACCS
Dec 3, 2012:
- 6:22 PM Changeset [2527] by
- Progress on CL to CM.
- 5:48 PM Changeset [2526] by
- …
- 5:39 PM Changeset [2525] by
- …
- 4:41 PM Changeset [2524] by
- Avoiding conflicts
- 4:30 PM Changeset [2523] by
- …
- 4:15 PM Changeset [2522] by
- Generic stuff moved to infrastructure.
- 4:10 PM Changeset [2521] by
- ..
- 4:07 PM Changeset [2520] by
- Now it is nice!
- 12:29 PM Changeset [2519] by
- To prevent conflicts
- 12:28 PM Changeset [2518] by
- …
- 11:51 AM Changeset [2517] by
- …
Dec 2, 2012:
- 5:45 PM Changeset [2516] by
- removed typedefs; restored older versions; moved typedefs to …
- 5:20 PM Changeset [2515] by
- …
- 4:40 PM Changeset [2514] by
- All .ma files committed: some of them are just in-progress.
Dec 1, 2012:
- 9:01 PM Changeset [2513] by
- Minor tweaks. Simplified dependencies again.
- 8:36 PM Changeset [2512] by
- Simplified dependencies on ASM, to allow rollback to when …
Nov 30, 2012:
- 6:31 PM Changeset [2511] by
- Conjecture main Cminor/RTLabs simulation results. Add a few notes …
- 4:40 PM Changeset [2510] by
- Some progress on the Cl -> Cm front
- 1:15 PM Changeset [2509] by
- misc note
Nov 29, 2012:
- 8:12 PM Changeset [2508] by
- more tweaks. compiler and correctness still build.
- 7:14 PM Changeset [2507] by
- finished pop case in commutation eval_Seq_no_pc
- 6:38 PM Changeset [2506] by
- Use common definition of measurable.
- 3:37 PM Changeset [2505] by
- Cleaned up compiler.ma; some refactoring/additional code needed in …
- 3:33 PM Changeset [2504] by
- More refactoring to support the tidied up compiler.ma
- 3:32 PM Changeset [2503] by
- tidied up, with new auxiliary defns, some refactoring, some code …
- 11:59 AM Changeset [2502] by
- Sketch a little about how measurable traces might work with RTLabs and …
- 10:12 AM Changeset [2501] by
- working on lineariseProof. Not yet finished.
Nov 28, 2012:
- 5:57 PM Changeset [2500] by
- Continuing work on simulation in Clight/Cminor?
- 12:52 PM Changeset [2499] by
- Separate out the RTLabs abstract status record from the proofs about …
Nov 27, 2012:
- 6:01 PM Changeset [2498] by
- Refactor: Typedefs object_code and costlabel_map lifted out from …
- 5:59 PM Changeset [2497] by
- Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
- 5:50 PM Changeset [2496] by
- Some tentative work on the simulation proof for expressions, in order …
- 5:17 PM Changeset [2495] by
- continuing lineariseProof
Nov 26, 2012:
- 6:24 PM Changeset [2494] by
- Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
- 6:00 PM Changeset [2493] by
- Change in cst_well_defd to fix previously broken defn of …
- 11:52 AM Changeset [2492] by
- Reduce axiomatisation in compiler.ma.
- 11:30 AM Changeset [2491] by
- fixed wrt change of list member definition
Nov 25, 2012:
- 1:33 PM Changeset [2490] by
- switched back to Byte immediate (instead of beval ones) propagated …
Nov 23, 2012:
- 5:28 PM Changeset [2489] by
- Conjecture some Clight/Cminor? simulation results.
- 4:29 PM Changeset [2488] by
- glitch fixed
- 3:47 PM Changeset [2487] by
- Set up "after_n_steps" to enforce an invariant on states.
- 12:18 PM Changeset [2486] by
- First go at a generalised version of measurable.
- 11:22 AM Changeset [2485] by
- Sketch of Clight/Cminor? callstate simulation
Nov 22, 2012:
- 6:40 PM Changeset [2484] by
- fixed Traces and semantics added commutation record (not yet finished) …
- 5:05 PM Changeset [2483] by
- Memory injections for Clight to Cminor, partially axiomatized.
- 3:49 PM Changeset [2482] by
- Note about front-end simulations
- 10:09 AM HiPEAC13 edited by
- (diff)
Nov 21, 2012:
Note: See TracTimeline
for information about the timeline view.
