Timeline


and

Jun 18, 2012:

5:16 PM Changeset [2100] by tranquil
temporary solution to a bug where operations on spilled registers …
2:07 PM WikiStart edited by mulligan
(diff)
2:05 PM Matita-18-06-2012.tar.gz attached to WikiStart by mulligan
Matita snapshot for typechecking CPP submissions
2:02 PM WikiStart edited by mulligan
(diff)
2:00 PM WikiStart edited by mulligan
(diff)

Jun 15, 2012:

5:56 PM Changeset [2099] by boender
- added reference to Intel dev manual
5:29 PM Changeset [2098] by boender
- updates & changes
3:25 PM Changeset [2097] by mulligan
Consistency change (institution)
3:25 PM Changeset [2096] by mulligan
Changes to the English for Jaap, and some tidying up and making …
1:58 PM Changeset [2095] by mulligan
Added reference to CompCert? and CompCertTSO.
1:56 PM Changeset [2094] by boender
- oops
1:55 PM Changeset [2093] by boender
- added reference to CompCertTSO
1:38 PM Changeset [2092] by mulligan
Jaap noticed it's Randall Hyde not Holmes.
1:35 PM Changeset [2091] by boender
- systematically changed 'jump' to 'branch'
12:57 PM Changeset [2090] by mulligan
Fixed mistaken reference to RISC instead of CISC architectures.
11:54 AM Changeset [2089] by mulligan
Harmonised institution name to that used by Jaap
11:52 AM Changeset [2088] by mulligan
Added list of keywords as is required. Other minor changes.
11:40 AM Changeset [2087] by mulligan
Tidied up the paper, added a few more things, tidied and expanded …
11:39 AM Changeset [2086] by boender
- spell-check
11:36 AM Changeset [2085] by boender
- rewrote introduction - changed 'medium' to 'absolute' - added a bit …
1:17 AM Changeset [2084] by boender
- changed bibliography style - added CerCo? thanks - some words of …

Jun 14, 2012:

5:32 PM Changeset [2083] by mulligan
More work on paper from today.
4:26 PM Changeset [2082] by boender
- reworked and extended presentation of invariants
12:04 PM Changeset [2081] by sacerdot
Type of assembly fixed to be compatible with the old one and to take …
11:57 AM Changeset [2080] by boender
- added references to SDCC and gcc (thanks, Dominic) - updated sigma …
11:45 AM Changeset [2079] by sacerdot
sigma_policy_specification restyled
11:44 AM Changeset [2078] by sacerdot
sigma_policy_specification has been 1) strengthened 2) made nicer to …
10:45 AM Changeset [2077] by boender
- committed actual file instead of link
10:30 AM Changeset [2076] by garnier
First steps towards a simulation proof for switch removal.
10:25 AM Changeset [2075] by mulligan
Solved conflict in AssemblyProof?
10:23 AM Changeset [2074] by garnier
Prophylactic renaming of a relation
4:10 AM Changeset [2073] by sacerdot
All false daemons removed.
4:03 AM Changeset [2072] by sacerdot
We need to import Jaap's invariants now.
3:25 AM Changeset [2071] by sacerdot
More daemons closed, but one is suspect now.
2:18 AM Changeset [2070] by sacerdot
More daemons closed.

Jun 13, 2012:

7:58 PM Changeset [2069] by sacerdot
7:54 PM Changeset [2068] by sacerdot
7:50 PM Changeset [2067] by sacerdot
6:46 PM Changeset [2066] by mulligan
Finished for the day.
5:54 PM Changeset [2065] by boender
- committed another draft
5:29 PM Changeset [2064] by boender
- more progress
5:05 PM Changeset [2063] by mulligan
Minor fixes
5:00 PM Changeset [2062] by sacerdot
Everything repaired (broken because of new proof obligation for fetch).
4:59 PM Changeset [2061] by mulligan
Added Randall Holmes' Usenet post on branch displacement optimisation …
4:26 PM Changeset [2060] by mulligan
More work on paper.
3:44 PM Changeset [2059] by boender
- updated Policy to work better
3:17 PM Changeset [2058] by mulligan
First draft of changes to main sections (i.e. those describing the …
1:30 PM Changeset [2057] by sacerdot
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
1:01 PM Changeset [2056] by sacerdot
Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
12:11 PM Changeset [2055] by sacerdot
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
11:58 AM Changeset [2054] by boender
- progress
11:02 AM Changeset [2053] by mulligan
Introduction changed, with many paragraphs deleted.
10:04 AM Changeset [2052] by mulligan
Initial commit of proposed CPP 2012 paper on the proof of correctness …

Jun 12, 2012:

5:49 PM Changeset [2051] by mulligan
Finished the Jmp case in the main theorem.
4:01 PM Changeset [2050] by campbell
Limit some normalization that doesn't seem to like.
3:49 PM Changeset [2049] by boender
- progress
2:46 PM Changeset [2048] by boender
- factorised jump decisions
2:18 PM Changeset [2047] by mulligan
Big bugs in policy calculations found. Waiting for Jaap's commit.
1:36 PM Changeset [2046] by boender
- removed old paper directory
1:35 PM Changeset [2045] by boender
- renamed paper directory
10:52 AM Changeset [2044] by campbell
PCs for RTLabs structured traces.

Jun 8, 2012:

11:41 PM Changeset [2043] by sacerdot
Broken code commented out.
11:33 PM Changeset [2042] by sacerdot
Repaired (Type => DeqSet?)
11:21 PM Changeset [2041] by sacerdot
Repaired: unified syntax for monads.
7:38 PM Changeset [2040] by sacerdot
Repaired using new /demod/ that allows to specify the rules to be used.
6:20 PM Changeset [2039] by sacerdot
New, better interface for subaddressing_mode_elim
6:17 PM Changeset [2038] by sacerdot
split => vsplit
5:56 PM Changeset [2037] by sacerdot
flatten is now part of stdlib
5:52 PM Changeset [2036] by sacerdot
New daemon inserted because /demod/ got worst :-(
5:51 PM Changeset [2035] by sacerdot
Fixed
5:16 PM Changeset [2034] by boender
- split Policy into three separate files for ease (and indeed …
4:57 PM Changeset [2033] by sacerdot
Daemon reverted.
4:32 PM Changeset [2032] by sacerdot
!! BEWARE: major commit !! 1) [affects everybody] split for …
3:52 PM Changeset [2031] by stark
Mention FMICS 2012 paper
1:44 PM Changeset [2030] by garnier
Cast simplification was too conservative, now reasonably aggressive.

Jun 7, 2012:

6:30 PM Changeset [2029] by stark
Mild revision of invitee list; commitment to HiPEAC
5:58 PM Changeset [2028] by boender
- bugfix to Assembly (forgotten sigma) - added …
5:53 PM Changeset [2027] by mulligan
Got the main lemma to apply in the proof of main theorem again and …
4:37 PM Changeset [2026] by mulligan
Added a new file to house the main theorem as the type checking time …
3:51 PM Changeset [2025] by campbell
Silly typo and old comment.
3:20 PM Changeset [2024] by mulligan
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
2:08 PM Changeset [2023] by mulligan
Closed main lemma modulo closing trivial subgoals about commutations …
10:47 AM Changeset [2022] by boender
- corrected jump calculation algorithm
1:44 AM Changeset [2021] by sacerdot
Proof skeleton in place. Several daemons to be closed adding invariants.

Jun 6, 2012:

6:27 PM Changeset [2020] by mulligan
CJNE case complete, DJNZ case almost complete
6:24 PM Changeset [2019] by campbell
Split out special induction principle for Clight from soundness file. …

Jun 5, 2012:

5:49 PM Changeset [2018] by mulligan
CJNE case a complete mess.

Jun 4, 2012:

5:38 PM Changeset [2017] by mulligan
Large swathes of proof of main lemma added.
4:13 PM Changeset [2016] by garnier
Slight change in simplification strategy to better match the semantics
4:06 PM Changeset [2015] by mulligan
Changes following a conversation with Jaap: as it stands computation …

Jun 2, 2012:

10:39 PM Changeset [2014] by mulligan
Fixed problem in James' email message.
12:11 AM Changeset [2013] by stark
Put in HiPEAC 2013

Jun 1, 2012:

11:49 PM Changeset [2012] by stark
Added proposed papers to D6.2

May 31, 2012:

4:41 PM Changeset [2011] by garnier
Minor cleanup.
3:10 PM Changeset [2010] by campbell
Make globalenvs use proper maps.

May 30, 2012:

9:34 PM Changeset [2009] by garnier
Proof of simulation completed for singe-step executions.
7:22 PM Changeset [2008] by boender
- substantial closing of holes in proof
6:55 PM Changeset [2007] by stark
Potential workshop invitees
6:43 PM Changeset [2006] by boender
- added alias for bitvector zero - changed extralib bounded …

May 29, 2012:

2:51 PM Changeset [2005] by boender
- minor changes to make things compile with a clean checkout

May 28, 2012:

2:35 PM Changeset [2004] by campbell
Minor edits from discussion.
1:10 PM Changeset [2003] by campbell
Some discussion of correctness statements.

May 26, 2012:

4:15 PM Changeset [2002] by stark
Supplement to D6.2

May 25, 2012:

1:47 PM Changeset [2001] by campbell
Get the compiler to output more.
11:01 AM Changeset [2000] by campbell
Fix g.e. glitch in label simulation.
10:45 AM Changeset [1999] by campbell
Make back-end use the main global envs.
10:18 AM Changeset [1998] by sacerdot
Version number bumped.
10:05 AM Changeset [1997] by mulligan
Changed titles of reports to match correct deliverable title
9:18 AM Changeset [1996] by campbell
Work on correctness from yesterday.

May 24, 2012:

7:18 PM Changeset [1995] by campbell
Overall compiler definition; bits and pieces to make everything happy(ish).
6:08 PM Changeset [1994] by campbell
Remove redundant allocation definition in Globalenvs.
5:10 PM Changeset [1993] by campbell
Make front-end memory model only depend on the general definitions by …
4:26 PM Changeset [1992] by mckinna
Ayache?
4:24 PM Changeset [1991] by campbell
Put the front end transformations together and make an example use it.
4:24 PM Changeset [1990] by mckinna
the LUSTRE paper has not yet appeared what about the Ayache/Frama?-C …
4:16 PM Changeset [1989] by mckinna
Notes of 2012-05-24 of the UEdin/UniBo meeting to discuss publication …
11:39 AM Changeset [1988] by campbell
Abstraction of the memory contents in the memory models is no longer …
10:22 AM Changeset [1987] by campbell
Move BEValues to common to reflect their use in the memory model for …
9:35 AM Changeset [1986] by campbell
Get rid of unused abstraction of Globalenvs.

May 22, 2012:

6:12 PM Changeset [1985] by mulligan
A single `false' case for unconditional jumps completed.
5:37 PM Changeset [1984] by mulligan
Most proof obligations closed in main_lemma apart from those of the …
11:15 AM Changeset [1983] by mulligan
Changes to simplify the simpler cases of the main_lemma.
8:14 AM Changeset [1982] by amadio
add 2.1 Survey
8:13 AM Changeset [1981] by amadio
update 5.1
8:12 AM Changeset [1980] by amadio
update 5.1
12:57 AM Changeset [1979] by sacerdot
Very very very tricky lemma closed. A dreadful mix of JM equality …
12:37 AM Changeset [1978] by sacerdot
Two more cases completed.
12:05 AM Changeset [1977] by sacerdot
Unblocked: let ... as hides two different terms, one that uses Leibniz …

May 21, 2012:

7:04 PM Changeset [1976] by tranquil
* monads: just changed some defs, which had to be propagated in some …
5:48 PM Changeset [1975] by mulligan
Work from today on closing main_thm.
5:03 PM Changeset [1974] by garnier
Progress on the cast simplification proof.
4:57 PM Changeset [1973] by boender
- removed superfluous match - displaced 'cases daemon'
10:33 AM Changeset [1972] by mulligan
Simple lemma with strangely complex proof complete.

May 20, 2012:

10:34 PM Changeset [1971] by sacerdot
1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
Note: See TracTimeline for information about the timeline view.