Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
Older Revisions
→
source:
src
/
ASM
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2129
8 years
mulligan
Large changes from today trying to complete the main theorem. Again :(
(edit)
@2128
8 years
sacerdot
Final shuffling around
(edit)
@2127
8 years
sacerdot
Last daemon closed
(edit)
@2126
8 years
sacerdot
Proof improved (for case 3) + new proof (for case 11)
(edit)
@2125
8 years
boender
- some more displacement from Policy to Util
(edit)
@2124
8 years
sacerdot
Much more shuffling around to proper places
(edit)
@2123
8 years
boender
- moved is_well_labeled_p to Status and instruction_is_label to ASM …
(edit)
@2122
8 years
sacerdot
More stuff moved around in proper places
(edit)
@2121
8 years
sacerdot
More functions moved to the places they belong to
Diff
Rev
Age
Author
Log Message
(edit)
@2119
8 years
sacerdot
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
Diff
Rev
Age
Author
Log Message
(edit)
@2115
8 years
sacerdot
Old commented out code removed
(edit)
@2114
8 years
sacerdot
Proof repaired
(edit)
@2113
8 years
sacerdot
Proof by cases repaired; dead code removed.
(edit)
@2112
8 years
sacerdot
WARNING: this commit may break some code. - dead/useless code removed
(edit)
@2111
8 years
sacerdot
Cleanup: lemmas/theorems/axioms moved to the right places.
(edit)
@2110
8 years
sacerdot
…
(edit)
@2109
8 years
mulligan
Finished porting the large, main lemma to the new notion of jump …
(edit)
@2108
8 years
mulligan
Various axioms closed and others moved around. Uncommented main lemma …
Diff
Rev
Age
Author
Log Message
(edit)
@2102
8 years
boender
- some small changes
(edit)
@2101
8 years
boender
- renamed medium to absolute jump - revised proofs of policy, some …
Diff
Rev
Age
Author
Log Message
(edit)
@2099
8 years
boender
- added reference to Intel dev manual
(edit)
@2098
8 years
boender
- updates & changes
(edit)
@2097
8 years
mulligan
Consistency change (institution)
(edit)
@2096
8 years
mulligan
Changes to the English for Jaap, and some tidying up and making …
(edit)
@2095
8 years
mulligan
Added reference to
CompCert?
and CompCertTSO.
(edit)
@2094
8 years
boender
- oops
(edit)
@2093
8 years
boender
- added reference to CompCertTSO
(edit)
@2092
8 years
mulligan
Jaap noticed it's Randall Hyde not Holmes.
(edit)
@2091
8 years
boender
- systematically changed 'jump' to 'branch'
(edit)
@2090
8 years
mulligan
Fixed mistaken reference to RISC instead of CISC architectures.
(edit)
@2089
8 years
mulligan
Harmonised institution name to that used by Jaap
(edit)
@2088
8 years
mulligan
Added list of keywords as is required. Other minor changes.
(edit)
@2087
8 years
mulligan
Tidied up the paper, added a few more things, tidied and expanded …
(edit)
@2086
8 years
boender
- spell-check
(edit)
@2085
8 years
boender
- rewrote introduction - changed 'medium' to 'absolute' - added a bit …
(edit)
@2084
8 years
boender
- changed bibliography style - added
CerCo?
thanks - some words of …
(edit)
@2083
8 years
mulligan
More work on paper from today.
(edit)
@2082
8 years
boender
- reworked and extended presentation of invariants
(edit)
@2081
8 years
sacerdot
Type of assembly fixed to be compatible with the old one and to take …
(edit)
@2080
8 years
boender
- added references to SDCC and gcc (thanks, Dominic) - updated sigma …
(edit)
@2079
8 years
sacerdot
sigma_policy_specification restyled
(edit)
@2078
8 years
sacerdot
sigma_policy_specification has been 1) strengthened 2) made nicer to …
(edit)
@2077
8 years
boender
- committed actual file instead of link
Diff
Rev
Age
Author
Log Message
(edit)
@2075
8 years
mulligan
Solved conflict in
AssemblyProof?
Diff
Rev
Age
Author
Log Message
(edit)
@2073
8 years
sacerdot
All false daemons removed.
(edit)
@2072
8 years
sacerdot
We need to import Jaap's invariants now.
(edit)
@2071
8 years
sacerdot
More daemons closed, but one is suspect now.
(edit)
@2070
8 years
sacerdot
More daemons closed.
(edit)
@2069
8 years
sacerdot
…
(edit)
@2068
8 years
sacerdot
…
(edit)
@2067
8 years
sacerdot
…
(edit)
@2066
8 years
mulligan
Finished for the day.
(edit)
@2065
8 years
boender
- committed another draft
(edit)
@2064
8 years
boender
- more progress
(edit)
@2063
8 years
mulligan
Minor fixes
(edit)
@2062
8 years
sacerdot
Everything repaired (broken because of new proof obligation for fetch).
(edit)
@2061
8 years
mulligan
Added Randall Holmes' Usenet post on branch displacement optimisation …
(edit)
@2060
8 years
mulligan
More work on paper.
(edit)
@2059
8 years
boender
- updated Policy to work better
(edit)
@2058
8 years
mulligan
First draft of changes to main sections (i.e. those describing the …
(edit)
@2057
8 years
sacerdot
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
(edit)
@2056
8 years
sacerdot
Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
(edit)
@2055
8 years
sacerdot
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
(edit)
@2054
8 years
boender
- progress
(edit)
@2053
8 years
mulligan
Introduction changed, with many paragraphs deleted.
(edit)
@2052
8 years
mulligan
Initial commit of proposed CPP 2012 paper on the proof of correctness …
(edit)
@2051
8 years
mulligan
Finished the Jmp case in the main theorem.
Diff
Rev
Age
Author
Log Message
(edit)
@2049
8 years
boender
- progress
(edit)
@2048
8 years
boender
- factorised jump decisions
(edit)
@2047
8 years
mulligan
Big bugs in policy calculations found. Waiting for Jaap's commit.
(edit)
@2046
8 years
boender
- removed old paper directory
(edit)
@2045
8 years
boender
- renamed paper directory
Diff
Rev
Age
Author
Log Message
(edit)
@2040
8 years
sacerdot
Repaired using new /demod/ that allows to specify the rules to be used.
(edit)
@2039
8 years
sacerdot
New, better interface for subaddressing_mode_elim
(edit)
@2038
8 years
sacerdot
split => vsplit
(edit)
@2037
8 years
sacerdot
flatten is now part of stdlib
(edit)
@2036
8 years
sacerdot
New daemon inserted because /demod/ got worst :-(
Diff
Rev
Age
Author
Log Message
(edit)
@2034
8 years
boender
- split Policy into three separate files for ease (and indeed …
Diff
Rev
Age
Author
Log Message
(edit)
@2032
8 years
sacerdot
!! BEWARE: major commit !! 1) [affects everybody] split for …
Diff
Rev
Age
Author
Log Message
(edit)
@2028
8 years
boender
- bugfix to Assembly (forgotten sigma) - added …
(edit)
@2027
8 years
mulligan
Got the main lemma to apply in the proof of main theorem again and …
(edit)
@2026
8 years
mulligan
Added a new file to house the main theorem as the type checking time …
Diff
Rev
Age
Author
Log Message
(edit)
@2024
8 years
mulligan
Updated
AssemblyProof?
to fix mismatch in definition of lookup_labels …
(edit)
@2023
8 years
mulligan
Closed main lemma modulo closing trivial subgoals about commutations …
(edit)
@2022
8 years
boender
- corrected jump calculation algorithm
(edit)
@2021
8 years
sacerdot
Proof skeleton in place. Several daemons to be closed adding invariants.
(edit)
@2020
8 years
mulligan
CJNE case complete, DJNZ case almost complete
Diff
Rev
Age
Author
Log Message
(edit)
@2018
8 years
mulligan
CJNE case a complete mess.
(edit)
@2017
8 years
mulligan
Large swathes of proof of main lemma added.
Diff
Rev
Age
Author
Log Message
(edit)
@2015
8 years
mulligan
Changes following a conversation with Jaap: as it stands computation …
(edit)
@2014
8 years
mulligan
Fixed problem in James' email message.
Diff
Rev
Age
Author
Log Message
(edit)
@2008
8 years
boender
- substantial closing of holes in proof
Diff
Rev
Age
Author
Log Message
(edit)
@2006
8 years
boender
- added alias for bitvector zero - changed extralib bounded …
(edit)
@2005
8 years
boender
- minor changes to make things compile with a clean checkout
Diff
Rev
Age
Author
Log Message
(edit)
@2001
8 years
campbell
Get the compiler to output more.
Diff
Rev
Age
Author
Log Message
(edit)
@1996
8 years
campbell
Work on correctness from yesterday.
Diff
Rev
Age
Author
Log Message
(edit)
@1987
8 years
campbell
Move BEValues to common to reflect their use in the memory model for …
Diff
Rev
Age
Author
Log Message
(edit)
@1985
8 years
mulligan
A single `false' case for unconditional jumps completed.
(edit)
@1984
8 years
mulligan
Most proof obligations closed in main_lemma apart from those of the …
(edit)
@1983
8 years
mulligan
Changes to simplify the simpler cases of the main_lemma.
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog