Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

AArch64 fastpath proofs #739

Merged
merged 8 commits into from
Mar 25, 2024
Merged

AArch64 fastpath proofs #739

merged 8 commits into from
Mar 25, 2024

Commits on Mar 25, 2024

  1. lib: generic monadic_rewrite_state_assert/stateAssert 

    These rules completely discarded the assertion and directly linked the
assertion with the precondition.
The general form allows assuming the assertion in subsequent statements
under the assumption on non-failure.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    0033f2d View commit details
    Browse the repository at this point in the history

  2. crefine: update for monadic_rewrite_stateAssert 

    Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    f2f38b7 View commit details
    Browse the repository at this point in the history

  3. haskell+design: add fastpathKernelAssertions 

    Add fastpathKernelAssertions to start of callKernel. Fastpath rewrite
proofs don't get the state relation, so can't cross properties over from
the abstract invariants. We also can't rely on asserts on the fast path
side, since any failure in the rewrite must be correlated with failure
in the original, and the locations and conditions of those failures can
be quite distant.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    c407d26 View commit details
    Browse the repository at this point in the history

  4. refine+crefine: define and handle fastpathKernelAssertions 

    Currently, this is only interesting on AARCH64 where we need no_fail
preconditions for looking up an ASID map entry.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    56e125d View commit details
    Browse the repository at this point in the history

  5. aarch64 crefine: fastpath specs for call and replyrecv 

    Update the existing fastpath function "design" specs with
AArch64-specific functionality:
* looking up the VMID / hardware asid is more complex, going via the
  ASID map, with additional checks necessary
* redundant check for ReplyMaster no longer happens

These specs will be shown to be equivalent to the slow path (callKernel)
and fastpath C code.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    dba6177 View commit details
    Browse the repository at this point in the history

  6. aarch64 crefine: prove fastpath equivalent to slow path 

    Plus cleanup and commentary.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    467ef27 View commit details
    Browse the repository at this point in the history

  7. aarch64 crefine: prove fastpath equivalent to C fastpath 

    Shows fastpath spec refines down to C for Call and ReplyRecv.
Includes much effort to document what is happening in the main proofs,
updates for AArch64-specific and 64-bit-specific mechanisms and
bitfields.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    754acc3 View commit details
    Browse the repository at this point in the history

  8. proof: remove AArch64 quick_and_dirty CRefine 

    CRefine on AARCH64 is now sorry-free, and there are no other sorried
developments at this time.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Mar 25, 2024
    Configuration menu
    Copy the full SHA
    4efd093 View commit details
    Browse the repository at this point in the history