Timeline
06/18/12:
- 17:16 Changeset [2100] by
- temporary solution to a bug where operations on spilled registers …
- 14:07 WikiStart edited by
- (diff)
- 14:02 WikiStart edited by
- (diff)
- 14:00 WikiStart edited by
- (diff)
06/15/12:
- 17:56 Changeset [2099] by
- - added reference to Intel dev manual
- 17:29 Changeset [2098] by
- - updates & changes
- 15:25 Changeset [2097] by
- Consistency change (institution)
- 15:25 Changeset [2096] by
- Changes to the English for Jaap, and some tidying up and making consistent …
- 13:58 Changeset [2095] by
- Added reference to CompCert? and CompCertTSO.
- 13:56 Changeset [2094] by
- - oops
- 13:55 Changeset [2093] by
- - added reference to CompCertTSO
- 13:38 Changeset [2092] by
- Jaap noticed it's Randall Hyde not Holmes.
- 13:35 Changeset [2091] by
- - systematically changed 'jump' to 'branch'
- 12:57 Changeset [2090] by
- Fixed mistaken reference to RISC instead of CISC architectures.
- 11:54 Changeset [2089] by
- Harmonised institution name to that used by Jaap
- 11:52 Changeset [2088] by
- Added list of keywords as is required. Other minor changes.
- 11:40 Changeset [2087] by
- Tidied up the paper, added a few more things, tidied and expanded …
- 11:39 Changeset [2086] by
- - spell-check
- 11:36 Changeset [2085] by
- - rewrote introduction - changed 'medium' to 'absolute' - added a bit to …
- 01:17 Changeset [2084] by
- - changed bibliography style - added CerCo? thanks - some words of …
06/14/12:
- 17:32 Changeset [2083] by
- More work on paper from today.
- 16:26 Changeset [2082] by
- - reworked and extended presentation of invariants
- 12:04 Changeset [2081] by
- Type of assembly fixed to be compatible with the old one and to take as a …
- 11:57 Changeset [2080] by
- - added references to SDCC and gcc (thanks, Dominic) - updated sigma …
- 11:45 Changeset [2079] by
- sigma_policy_specification restyled
- 11:44 Changeset [2078] by
- sigma_policy_specification has been 1) strengthened 2) made nicer to see …
- 10:45 Changeset [2077] by
- - committed actual file instead of link
- 10:30 Changeset [2076] by
- First steps towards a simulation proof for switch removal.
- 10:25 Changeset [2075] by
- Solved conflict in AssemblyProof?
- 10:23 Changeset [2074] by
- Prophylactic renaming of a relation
- 04:10 Changeset [2073] by
- All false daemons removed.
- 04:03 Changeset [2072] by
- We need to import Jaap's invariants now.
- 03:25 Changeset [2071] by
- More daemons closed, but one is suspect now.
- 02:18 Changeset [2070] by
- More daemons closed.
06/13/12:
- 19:58 Changeset [2069] by
- …
- 19:54 Changeset [2068] by
- …
- 19:50 Changeset [2067] by
- …
- 18:46 Changeset [2066] by
- Finished for the day.
- 17:54 Changeset [2065] by
- - committed another draft
- 17:29 Changeset [2064] by
- - more progress
- 17:05 Changeset [2063] by
- Minor fixes
- 17:00 Changeset [2062] by
- Everything repaired (broken because of new proof obligation for fetch).
- 16:59 Changeset [2061] by
- Added Randall Holmes' Usenet post on branch displacement optimisation to …
- 16:26 Changeset [2060] by
- More work on paper.
- 15:44 Changeset [2059] by
- - updated Policy to work better
- 15:17 Changeset [2058] by
- First draft of changes to main sections (i.e. those describing the proof …
- 13:30 Changeset [2057] by
- Repaired (was broken by fetch_pseudo_instruction now taking a proof …
- 13:01 Changeset [2056] by
- Repaired, ported to new fetch_pseudo_assembly. The execute_n is commented …
- 12:11 Changeset [2055] by
- Warning: this commit adds an hypothesis that breaks all of assembly stuff.
- 11:58 Changeset [2054] by
- - progress
- 11:02 Changeset [2053] by
- Introduction changed, with many paragraphs deleted.
- 10:04 Changeset [2052] by
- Initial commit of proposed CPP 2012 paper on the proof of correctness for …
06/12/12:
- 17:49 Changeset [2051] by
- Finished the Jmp case in the main theorem.
- 16:01 Changeset [2050] by
- Limit some normalization that // doesn't seem to like.
- 15:49 Changeset [2049] by
- - progress
- 14:46 Changeset [2048] by
- - factorised jump decisions
- 14:18 Changeset [2047] by
- Big bugs in policy calculations found. Waiting for Jaap's commit.
- 13:36 Changeset [2046] by
- - removed old paper directory
- 13:35 Changeset [2045] by
- - renamed paper directory
- 10:52 Changeset [2044] by
- PCs for RTLabs structured traces.
06/08/12:
- 23:41 Changeset [2043] by
- Broken code commented out.
- 23:33 Changeset [2042] by
- Repaired (Type => DeqSet?)
- 23:21 Changeset [2041] by
- Repaired: unified syntax for monads.
- 19:38 Changeset [2040] by
- Repaired using new /demod/ that allows to specify the rules to be used.
- 18:20 Changeset [2039] by
- New, better interface for subaddressing_mode_elim
- 18:17 Changeset [2038] by
- split => vsplit
- 17:56 Changeset [2037] by
- flatten is now part of stdlib
- 17:52 Changeset [2036] by
- New daemon inserted because /demod/ got worst :-(
- 17:51 Changeset [2035] by
- Fixed
- 17:16 Changeset [2034] by
- - split Policy into three separate files for ease (and indeed possibility) …
- 16:57 Changeset [2033] by
- Daemon reverted.
- 16:32 Changeset [2032] by
- !! BEWARE: major commit !! 1) [affects everybody] split for vectors …
- 15:52 Changeset [2031] by
- Mention FMICS 2012 paper
- 13:44 Changeset [2030] by
- Cast simplification was too conservative, now reasonably aggressive.
06/07/12:
- 18:30 Changeset [2029] by
- Mild revision of invitee list; commitment to HiPEAC
- 17:58 Changeset [2028] by
- - bugfix to Assembly (forgotten sigma) - added add_bitvector_of_nat_plus …
- 17:53 Changeset [2027] by
- Got the main lemma to apply in the proof of main theorem again and closed …
- 16:37 Changeset [2026] by
- Added a new file to house the main theorem as the type checking time for …
- 15:51 Changeset [2025] by
- Silly typo and old comment.
- 15:20 Changeset [2024] by
- Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
- 14:08 Changeset [2023] by
- Closed main lemma modulo closing trivial subgoals about commutations and …
- 10:47 Changeset [2022] by
- - corrected jump calculation algorithm
- 01:44 Changeset [2021] by
- Proof skeleton in place. Several daemons to be closed adding invariants.
06/06/12:
- 18:27 Changeset [2020] by
- CJNE case complete, DJNZ case almost complete
- 18:24 Changeset [2019] by
- Split out special induction principle for Clight from soundness file. Put …
06/05/12:
- 17:49 Changeset [2018] by
- CJNE case a complete mess.
06/04/12:
- 17:38 Changeset [2017] by
- Large swathes of proof of main lemma added.
- 16:13 Changeset [2016] by
- Slight change in simplification strategy to better match the semantics
- 16:06 Changeset [2015] by
- Changes following a conversation with Jaap: as it stands computation of …
06/02/12:
- 22:39 Changeset [2014] by
- Fixed problem in James' email message.
- 00:11 Changeset [2013] by
- Put in HiPEAC 2013
06/01/12:
- 23:49 Changeset [2012] by
- Added proposed papers to D6.2
05/31/12:
- 16:41 Changeset [2011] by
- Minor cleanup.
- 15:10 Changeset [2010] by
- Make globalenvs use proper maps.
05/30/12:
- 21:34 Changeset [2009] by
- Proof of simulation completed for singe-step executions.
- 19:22 Changeset [2008] by
- - substantial closing of holes in proof
- 18:55 Changeset [2007] by
- Potential workshop invitees
- 18:43 Changeset [2006] by
- - added alias for bitvector zero - changed extralib bounded forall/exists …
05/29/12:
- 14:51 Changeset [2005] by
- - minor changes to make things compile with a clean checkout
05/28/12:
- 14:35 Changeset [2004] by
- Minor edits from discussion.
- 13:10 Changeset [2003] by
- Some discussion of correctness statements.
05/26/12:
- 16:15 Changeset [2002] by
- Supplement to D6.2
05/25/12:
- 13:47 Changeset [2001] by
- Get the compiler to output more.
- 11:01 Changeset [2000] by
- Fix g.e. glitch in label simulation.
- 10:45 Changeset [1999] by
- Make back-end use the main global envs.
- 10:18 Changeset [1998] by
- Version number bumped.
- 10:05 Changeset [1997] by
- Changed titles of reports to match correct deliverable title
- 09:18 Changeset [1996] by
- Work on correctness from yesterday.
05/24/12:
- 19:18 Changeset [1995] by
- Overall compiler definition; bits and pieces to make everything …
- 18:08 Changeset [1994] by
- Remove redundant allocation definition in Globalenvs.
- 17:10 Changeset [1993] by
- Make front-end memory model only depend on the general definitions by …
- 16:26 Changeset [1992] by
- Ayache?
- 16:24 Changeset [1991] by
- Put the front end transformations together and make an example use it.
- 16:24 Changeset [1990] by
- the LUSTRE paper has not yet appeared what about the Ayache/Frama?-C …
- 16:16 Changeset [1989] by
- Notes of 2012-05-24 of the UEdin/UniBo meeting to discuss publication plan …
- 11:39 Changeset [1988] by
- Abstraction of the memory contents in the memory models is no longer …
- 10:22 Changeset [1987] by
- Move BEValues to common to reflect their use in the memory model for …
- 09:35 Changeset [1986] by
- Get rid of unused abstraction of Globalenvs.
05/22/12:
- 18:12 Changeset [1985] by
- A single `false' case for unconditional jumps completed.
- 17:37 Changeset [1984] by
- Most proof obligations closed in main_lemma apart from those of the …
- 11:15 Changeset [1983] by
- Changes to simplify the simpler cases of the main_lemma.
- 08:14 Changeset [1982] by
- add 2.1 Survey
- 08:13 Changeset [1981] by
- update 5.1
- 08:12 Changeset [1980] by
- update 5.1
- 00:57 Changeset [1979] by
- Very very very tricky lemma closed. A dreadful mix of JM equality …
- 00:37 Changeset [1978] by
- Two more cases completed.
- 00:05 Changeset [1977] by
- Unblocked: let ... as hides two different terms, one that uses Leibniz and …
05/21/12:
- 19:04 Changeset [1976] by
- * monads: just changed some defs, which had to be propagated in some files …
- 17:48 Changeset [1975] by
- Work from today on closing main_thm.
- 17:03 Changeset [1974] by
- Progress on the cast simplification proof.
- 16:57 Changeset [1973] by
- - removed superfluous match - displaced 'cases daemon'
- 10:33 Changeset [1972] by
- Simple lemma with strangely complex proof complete.
05/20/12:
- 22:34 Changeset [1971] by
- 1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) …
Note: See TracTimeline
for information about the timeline view.
