#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
011e0845 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new comment syntax (result of "isabelle update_comments <dirs>")
|
#
b5cdf470 |
|
13-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
globally use session-qualified imports; add Lib session Session-qualified imports will be required for Isabelle2018 and help clarify the structure of sessions in the build tree. This commit mainly adds a new set of sessions for lib/, including a Lib session that includes most theories in lib/ and a few separate sessions for parts that have dependencies beyond CParser or are separate AFP sessions. The group "lib" collects all lib/ sessions. As a consequence, other theories should use lib/ theories by session name, not by path, which in turns means spec and proof sessions should also refer to each other by session name, not path, to avoid duplicate theory errors in theory merges later.
|
#
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
#
84633ccb |
|
26-Feb-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
ARM access: proof update for user_context refactor
|
#
4601f2a1 |
|
06-Feb-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
|
#
2a1beffa |
|
26-Nov-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm: update for simple_ko getter/setter
|
#
3841b6e8 |
|
05-Dec-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm : add AEndpoint and ANTFN a_type simplification in addition to the a_type ATCB simplification, the following two are now in the simpset: "a_type (Endpoint x) = AEndpoint" "a_type (Notification v) = ANTFN"
|
#
3a22487c |
|
24-Nov-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242) Colloquially known as "invert-fastpath". Update verification efforts on ARM for the following seL4 changes: - scheduling decisions done in possibleSwitchTo are moved to the scheduler - possibleSwitchTo only checks whether the candidate is valid for a fast switch, not its priority, accepting possible candidates immmediately as a switch-to scheduler action - the scheduler checks the candidate against the current thread and against the bitmaps before making a decision - attemptSwitchTo and switchIfRequiredTo are gone - scheduler is now more complicated, and numerous proofs related to it are rewritten from scratch - fast path now checks ready queues via the scheduler bitmaps - L2 scheduler bitmap order reversed for better cache locality Many iterations between the kernel and verification teams were needed to get this right.
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
b17a3293 |
|
19-May-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm access: ARM Access now builds on arm-hyp
|
#
71e2db88 |
|
01-May-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
arm: refactor sanitise_register to take a bool instead of a kernel_object This simplified the sanitise_register logic in CRefine for arm-hyp.
|
#
47119bf4 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
1289f7bc |
|
09-Nov-2016 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes * tcb_context rephrasing to (tcb_context o tcb_arch) and respectively for set operations * unfolding of reserved_irq for trivially solving most lemmas * Changes to the inductive definition of integrity_obj to account for tcb_arch and tcb_context new location * Changes to the tcb examples in ExampleSystem to include tcb_arch * Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case * Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch) * Trivial unfolding of handle_reserved_irq for hoare rules * Examples in Example_Valid_State.thy were updated * Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ handling * Fun fact, some proofs are now shorter tags: [VER-623][SELFOUR-413]
|
#
8d4a8eb2 |
|
21-Sep-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: fix coding style
|
#
252ce8df |
|
09-Aug-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: infoflow and infoflow_c builds
|
#
0e5ffd1e |
|
27-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: requalify abstract theories
|
#
14f75701 |
|
21-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: Access checking
|
#
6f6c5816 |
|
09-Feb-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
SELFOUR-56: Remove diminish rights from IPC
|
#
0f2d5576 |
|
23-Nov-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
terminology in comments: async ep -> notifications
|
#
ac632c5a |
|
10-Nov-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Wait -> Recv: update proofs
|
#
457a55a8 |
|
01-Nov-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
add arch_tcb object to C, rename aep -> ntfn
|
#
7c3a06a8 |
|
28-Oct-2015 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Minor adjustments caused by Strengthen changes.
|
#
e403eb8f |
|
20-Oct-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
poll: added non blocking sync wait
|
#
d6f7579b |
|
15-Oct-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
poll: Added new syscall for polling async endpoints (non-blocking wait)
|
#
e3704742 |
|
06-Oct-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
aep-binding: cleanup
|
#
d88a931e |
|
01-Sep-2015 |
Ramana Kumar <Ramana.Kumar@nicta.com.au> |
history squashed patch for aep-binding
|
#
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
#
177e5bf1 |
|
06-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
2015 update for access
|
#
71e7dcc3 |
|
13-Aug-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Fix Access, InfoFlow and DRefine.
|
#
fc6e5771 |
|
10-Aug-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Proof updates, working as far as AInvs.
|
#
1af1d2b6 |
|
08-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
some of the global Isabelle2014 renames option_case -> case_option sum_case -> case_sum prod_case -> case_prod Option.set -> set_option Option.map -> map_option option_rel -> rel_option list_all2_def -> list_all2_iff map.simps -> list.map tl.simps -> list.sel(2-3) the.simps -> option.sel
|
#
50dda770 |
|
22-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
comment cleanup
|
#
9d9a3250 |
|
18-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Updates for getpaddr system call (by Joel Beeren)
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|