Timeline
Jun 27, 2012:
- 10:19 PM Changeset [2130] by
- Proof repaired after Dominic's bug fix.
- 7:14 PM Changeset [2129] by
- Large changes from today trying to complete the main theorem. Again :(
- 5:05 PM Changeset [2128] by
- Final shuffling around
- 4:59 PM Changeset [2127] by
- Last daemon closed
- 4:56 PM Changeset [2126] by
- Proof improved (for case 3) + new proof (for case 11)
- 4:28 PM Changeset [2125] by
- - some more displacement from Policy to Util
- 4:23 PM Changeset [2124] by
- Much more shuffling around to proper places
- 4:04 PM Changeset [2123] by
- - moved is_well_labeled_p to Status and instruction_is_label to ASM …
- 3:36 PM Changeset [2122] by
- More stuff moved around in proper places
- 3:30 PM Changeset [2121] by
- More functions moved to the places they belong to
- 12:59 PM Changeset [2120] by
- Fix victim of alloc unfolding.
- 12:09 PM Changeset [2119] by
- load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
- 12:04 PM Changeset [2118] by
- Labelling preserves behaviour.
- 12:04 PM Changeset [2117] by
- Workaround for bug in Matita.
- 11:46 AM Changeset [2116] by
- load_code_memory will be moved into Fetch.ma in the next commit. This …
- 1:59 AM Changeset [2115] by
- Old commented out code removed
- 1:40 AM Changeset [2114] by
- Proof repaired
- 12:49 AM Changeset [2113] by
- Proof by cases repaired; dead code removed.
Jun 26, 2012:
- 11:47 PM Changeset [2112] by
- WARNING: this commit may break some code. - dead/useless code removed
- 5:30 PM Changeset [2111] by
- Cleanup: lemmas/theorems/axioms moved to the right places.
- 4:05 PM Changeset [2110] by
- …
- 2:47 PM Changeset [2109] by
- Finished porting the large, main lemma to the new notion of jump …
Jun 25, 2012:
- 2:39 PM Changeset [2108] by
- Various axioms closed and others moved around. Uncommented main lemma …
Jun 22, 2012:
- 2:07 PM Changeset [2107] by
- Memory initialisation and program transformations.
Jun 21, 2012:
- 5:21 PM Changeset [2106] by
- Fix up a couple of proofs broken by recent changes.
- 5:21 PM Changeset [2105] by
- Show some results about globalenvs and program transformations.
- 5:21 PM Changeset [2104] by
- Fill in misc axiom.
- 5:21 PM Changeset [2103] by
- Make transform_*program take a more general transformation to make …
Jun 20, 2012:
- 4:51 PM Changeset [2102] by
- - some small changes
Jun 19, 2012:
- 4:43 PM Changeset [2101] by
- - renamed medium to absolute jump - revised proofs of policy, some …
Jun 18, 2012:
- 5:16 PM Changeset [2100] by
- temporary solution to a bug where operations on spilled registers …
- 2:07 PM WikiStart edited by
- (diff)
- 2:02 PM WikiStart edited by
- (diff)
- 2:00 PM WikiStart edited by
- (diff)
Jun 15, 2012:
- 5:56 PM Changeset [2099] by
- - added reference to Intel dev manual
- 5:29 PM Changeset [2098] by
- - updates & changes
- 3:25 PM Changeset [2097] by
- Consistency change (institution)
- 3:25 PM Changeset [2096] by
- Changes to the English for Jaap, and some tidying up and making …
- 1:58 PM Changeset [2095] by
- Added reference to CompCert? and CompCertTSO.
- 1:56 PM Changeset [2094] by
- - oops
- 1:55 PM Changeset [2093] by
- - added reference to CompCertTSO
- 1:38 PM Changeset [2092] by
- Jaap noticed it's Randall Hyde not Holmes.
- 1:35 PM Changeset [2091] by
- - systematically changed 'jump' to 'branch'
- 12:57 PM Changeset [2090] by
- Fixed mistaken reference to RISC instead of CISC architectures.
- 11:54 AM Changeset [2089] by
- Harmonised institution name to that used by Jaap
- 11:52 AM Changeset [2088] by
- Added list of keywords as is required. Other minor changes.
- 11:40 AM Changeset [2087] by
- Tidied up the paper, added a few more things, tidied and expanded …
- 11:39 AM Changeset [2086] by
- - spell-check
- 11:36 AM Changeset [2085] by
- - rewrote introduction - changed 'medium' to 'absolute' - added a bit …
- 1:17 AM Changeset [2084] by
- - changed bibliography style - added CerCo? thanks - some words of …
Jun 14, 2012:
- 5:32 PM Changeset [2083] by
- More work on paper from today.
- 4:26 PM Changeset [2082] by
- - reworked and extended presentation of invariants
- 12:04 PM Changeset [2081] by
- Type of assembly fixed to be compatible with the old one and to take …
- 11:57 AM Changeset [2080] by
- - added references to SDCC and gcc (thanks, Dominic) - updated sigma …
- 11:45 AM Changeset [2079] by
- sigma_policy_specification restyled
- 11:44 AM Changeset [2078] by
- sigma_policy_specification has been 1) strengthened 2) made nicer to …
- 10:45 AM Changeset [2077] by
- - committed actual file instead of link
- 10:30 AM Changeset [2076] by
- First steps towards a simulation proof for switch removal.
- 10:25 AM Changeset [2075] by
- Solved conflict in AssemblyProof?
- 10:23 AM Changeset [2074] by
- Prophylactic renaming of a relation
- 4:10 AM Changeset [2073] by
- All false daemons removed.
- 4:03 AM Changeset [2072] by
- We need to import Jaap's invariants now.
- 3:25 AM Changeset [2071] by
- More daemons closed, but one is suspect now.
- 2:18 AM Changeset [2070] by
- More daemons closed.
Jun 13, 2012:
- 7:58 PM Changeset [2069] by
- …
- 7:54 PM Changeset [2068] by
- …
- 7:50 PM Changeset [2067] by
- …
- 6:46 PM Changeset [2066] by
- Finished for the day.
- 5:54 PM Changeset [2065] by
- - committed another draft
- 5:29 PM Changeset [2064] by
- - more progress
- 5:05 PM Changeset [2063] by
- Minor fixes
- 5:00 PM Changeset [2062] by
- Everything repaired (broken because of new proof obligation for fetch).
- 4:59 PM Changeset [2061] by
- Added Randall Holmes' Usenet post on branch displacement optimisation …
- 4:26 PM Changeset [2060] by
- More work on paper.
- 3:44 PM Changeset [2059] by
- - updated Policy to work better
- 3:17 PM Changeset [2058] by
- First draft of changes to main sections (i.e. those describing the …
- 1:30 PM Changeset [2057] by
- Repaired (was broken by fetch_pseudo_instruction now taking a proof …
- 1:01 PM Changeset [2056] by
- Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
- 12:11 PM Changeset [2055] by
- Warning: this commit adds an hypothesis that breaks all of assembly stuff.
- 11:58 AM Changeset [2054] by
- - progress
- 11:02 AM Changeset [2053] by
- Introduction changed, with many paragraphs deleted.
- 10:04 AM Changeset [2052] by
- Initial commit of proposed CPP 2012 paper on the proof of correctness …
Jun 12, 2012:
- 5:49 PM Changeset [2051] by
- Finished the Jmp case in the main theorem.
- 4:01 PM Changeset [2050] by
- Limit some normalization that doesn't seem to like.
- 3:49 PM Changeset [2049] by
- - progress
- 2:46 PM Changeset [2048] by
- - factorised jump decisions
- 2:18 PM Changeset [2047] by
- Big bugs in policy calculations found. Waiting for Jaap's commit.
- 1:36 PM Changeset [2046] by
- - removed old paper directory
- 1:35 PM Changeset [2045] by
- - renamed paper directory
- 10:52 AM Changeset [2044] by
- PCs for RTLabs structured traces.
Jun 8, 2012:
- 11:41 PM Changeset [2043] by
- Broken code commented out.
- 11:33 PM Changeset [2042] by
- Repaired (Type => DeqSet?)
- 11:21 PM Changeset [2041] by
- Repaired: unified syntax for monads.
- 7:38 PM Changeset [2040] by
- Repaired using new /demod/ that allows to specify the rules to be used.
- 6:20 PM Changeset [2039] by
- New, better interface for subaddressing_mode_elim
- 6:17 PM Changeset [2038] by
- split => vsplit
- 5:56 PM Changeset [2037] by
- flatten is now part of stdlib
- 5:52 PM Changeset [2036] by
- New daemon inserted because /demod/ got worst :-(
- 5:51 PM Changeset [2035] by
- Fixed
- 5:16 PM Changeset [2034] by
- - split Policy into three separate files for ease (and indeed …
- 4:57 PM Changeset [2033] by
- Daemon reverted.
- 4:32 PM Changeset [2032] by
- !! BEWARE: major commit !! 1) [affects everybody] split for …
- 3:52 PM Changeset [2031] by
- Mention FMICS 2012 paper
- 1:44 PM Changeset [2030] by
- Cast simplification was too conservative, now reasonably aggressive.
Jun 7, 2012:
- 6:30 PM Changeset [2029] by
- Mild revision of invitee list; commitment to HiPEAC
- 5:58 PM Changeset [2028] by
- - bugfix to Assembly (forgotten sigma) - added …
- 5:53 PM Changeset [2027] by
- Got the main lemma to apply in the proof of main theorem again and …
- 4:37 PM Changeset [2026] by
- Added a new file to house the main theorem as the type checking time …
- 3:51 PM Changeset [2025] by
- Silly typo and old comment.
- 3:20 PM Changeset [2024] by
- Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
- 2:08 PM Changeset [2023] by
- Closed main lemma modulo closing trivial subgoals about commutations …
- 10:47 AM Changeset [2022] by
- - corrected jump calculation algorithm
- 1:44 AM Changeset [2021] by
- Proof skeleton in place. Several daemons to be closed adding invariants.
Jun 6, 2012:
- 6:27 PM Changeset [2020] by
- CJNE case complete, DJNZ case almost complete
- 6:24 PM Changeset [2019] by
- Split out special induction principle for Clight from soundness file. …
Jun 5, 2012:
- 5:49 PM Changeset [2018] by
- CJNE case a complete mess.
Jun 4, 2012:
- 5:38 PM Changeset [2017] by
- Large swathes of proof of main lemma added.
- 4:13 PM Changeset [2016] by
- Slight change in simplification strategy to better match the semantics
- 4:06 PM Changeset [2015] by
- Changes following a conversation with Jaap: as it stands computation …
Jun 2, 2012:
- 10:39 PM Changeset [2014] by
- Fixed problem in James' email message.
- 12:11 AM Changeset [2013] by
- Put in HiPEAC 2013
Jun 1, 2012:
- 11:49 PM Changeset [2012] by
- Added proposed papers to D6.2
May 31, 2012:
- 4:41 PM Changeset [2011] by
- Minor cleanup.
- 3:10 PM Changeset [2010] by
- Make globalenvs use proper maps.
May 30, 2012:
- 9:34 PM Changeset [2009] by
- Proof of simulation completed for singe-step executions.
- 7:22 PM Changeset [2008] by
- - substantial closing of holes in proof
- 6:55 PM Changeset [2007] by
- Potential workshop invitees
- 6:43 PM Changeset [2006] by
- - added alias for bitvector zero - changed extralib bounded …
May 29, 2012:
- 2:51 PM Changeset [2005] by
- - minor changes to make things compile with a clean checkout
May 28, 2012:
- 2:35 PM Changeset [2004] by
- Minor edits from discussion.
- 1:10 PM Changeset [2003] by
- Some discussion of correctness statements.
Note: See TracTimeline
for information about the timeline view.
