1%
2% Copyright 2014, General Dynamics C4 Systems
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(GD_GPL)
9%
10
11This module contains utility functions used in system call implementations.
12
13> module SEL4.Model.Syscall where
14
15\begin{impdetails}
16
17> import SEL4.API.Failures
18> import SEL4.Model.StateData
19> import SEL4.Model.Failures
20> import SEL4.Model.Preemption
21> import Control.Monad.Except
22
23\end{impdetails}
24
25System calls in seL4 have three stages: one which may fault, one which may encounter system call errors, and one which cannot fail but may be interrupted. Generally the first is used to look up capabilities, the second to decode arguments and check for possible failures, and the third to perform the operation itself. If either of the first two stages fails, a failure handler runs instead of the following stages.
26
27The "syscall" function lifts code into the appropriate monads, and handles faults and errors.
28
29> syscall :: KernelF Fault a -> (Fault -> Kernel c) ->
30>         (a -> KernelF SyscallError b) -> (SyscallError -> Kernel c) ->
31>         (b -> KernelP c) -> KernelP c
32> syscall mFault hFault mError hError mFinalise = do
33>     rFault <- withoutPreemption $ runExceptT mFault
34>     case rFault of
35>         Left f -> withoutPreemption $ hFault f
36>         Right a -> do
37>             rError <- withoutPreemption $ runExceptT $ mError a
38>             case rError of
39>                 Left e -> withoutPreemption $ hError e
40>                 Right b -> mFinalise b
41
42
43