From 2732406e983071d1e84b9b3e3b9b99edb586aa36 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Fri, 18 Jul 2014 15:11:53 +1000 Subject: [PATCH 01/13] Recomment of branch getpaddr on release snapshot --- .../arch_include/arm/interfaces/sel4arch.xml | 3 +++ .../arch_include/ia32/interfaces/sel4arch.xml | 3 +++ manual/parts/api.tex | 2 ++ manual/parts/api/arm_page_getaddress.tex | 20 ++++++++++++++ manual/parts/api/ia32_page_getaddress.tex | 20 ++++++++++++++ src/arch/arm/kernel/vspace.c | 27 +++++++++++++++++++ src/arch/ia32/kernel/vspace.c | 26 ++++++++++++++++++ 7 files changed, 101 insertions(+) create mode 100644 manual/parts/api/arm_page_getaddress.tex create mode 100644 manual/parts/api/ia32_page_getaddress.tex diff --git a/libsel4/arch_include/arm/interfaces/sel4arch.xml b/libsel4/arch_include/arm/interfaces/sel4arch.xml index daead2ea0..53fde3f4c 100644 --- a/libsel4/arch_include/arm/interfaces/sel4arch.xml +++ b/libsel4/arch_include/arm/interfaces/sel4arch.xml @@ -86,6 +86,9 @@ + + + diff --git a/libsel4/arch_include/ia32/interfaces/sel4arch.xml b/libsel4/arch_include/ia32/interfaces/sel4arch.xml index 1152dbed9..ab5205053 100644 --- a/libsel4/arch_include/ia32/interfaces/sel4arch.xml +++ b/libsel4/arch_include/ia32/interfaces/sel4arch.xml @@ -58,6 +58,9 @@ + + + diff --git a/manual/parts/api.tex b/manual/parts/api.tex index 3c3e09c43..14ece6b18 100644 --- a/manual/parts/api.tex +++ b/manual/parts/api.tex @@ -296,6 +296,7 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request. \inputapidoc{ia32_page_map} \inputapidoc{ia32_page_remap} \inputapidoc{ia32_page_unmap} +\inputapidoc{ia32_page_getaddress} \inputapidoc{ia32_pagetable_map} \inputapidoc{ia32_pagetable_unmap} \fi @@ -310,5 +311,6 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request. \inputapidoc{arm_page_map} \inputapidoc{arm_page_remap} \inputapidoc{arm_page_unmap} +\inputapidoc{arm_page_getaddress} \inputapidoc{arm_pagetable_map} \inputapidoc{arm_pagetable_unmap} diff --git a/manual/parts/api/arm_page_getaddress.tex b/manual/parts/api/arm_page_getaddress.tex new file mode 100644 index 000000000..98b8a21c8 --- /dev/null +++ b/manual/parts/api/arm_page_getaddress.tex @@ -0,0 +1,20 @@ +% +% Copyright 2014, General Dynamics C4 Systems +% +% This software may be distributed and modified according to the terms of +% the GNU General Public License version 2. Note that NO WARRANTY is provided. +% See "LICENSE_GPLv2.txt" for details. +% +% @TAG(GD_GPL) +% + +\apidoc +{arm_page_getaddress} +{ARM Page - Get Address} +{Get the physical address of the underlying frame} +{static inline seL4\_ARM\_Page\_GetAddress\_t seL4\_ARM\_Page\_GetAddress} +{ +\param{seL4\_ARM\_Page}{\_service}{Capability to the page to lookup.} +} +{A seL4\_ARM\_Page\_GetAddress\_t structure as described in TODO} +{See \autoref{ch:vspace}} diff --git a/manual/parts/api/ia32_page_getaddress.tex b/manual/parts/api/ia32_page_getaddress.tex new file mode 100644 index 000000000..8f16dab5b --- /dev/null +++ b/manual/parts/api/ia32_page_getaddress.tex @@ -0,0 +1,20 @@ +% +% Copyright 2014, General Dynamics C4 Systems +% +% This software may be distributed and modified according to the terms of +% the GNU General Public License version 2. Note that NO WARRANTY is provided. +% See "LICENSE_GPLv2.txt" for details. +% +% @TAG(GD_GPL) +% + +\apidoc +{ia32_page_getaddress} +{IA32 Page - Get Address} +{Get the physical address of the underlying frame} +{static inline seL4\_IA32\_Page\_GetAddress\_t seL4\_IA32\_Page\_GetAddress} +{ +\param{seL4\_IA32\_Page}{\_service}{Capability to the page to lookup.} +} +{A seL4\_IA32\_Page\_GetAddress\_t structure as described in TODO} +{See \autoref{ch:vspace}} diff --git a/src/arch/arm/kernel/vspace.c b/src/arch/arm/kernel/vspace.c index b1a2f4b2e..cb6db5a37 100644 --- a/src/arch/arm/kernel/vspace.c +++ b/src/arch/arm/kernel/vspace.c @@ -60,6 +60,7 @@ static exception_t performPDFlush(int label, pde_t *pd, asid_t asid, vptr_t start, vptr_t end, paddr_t pstart); static exception_t performPageFlush(int label, pde_t *pd, asid_t asid, vptr_t start, vptr_t end, paddr_t pstart); +static exception_t performPageGetAddress(void *vbase_ptr); static exception_t decodeARMPageDirectoryInvocation(word_t label, unsigned int length, cptr_t cptr, cte_t *cte, cap_t cap, extra_caps_t extraCaps, word_t *buffer); @@ -1659,6 +1660,16 @@ decodeARMFrameInvocation(word_t label, unsigned int length, return performPageFlush(label, pd.pd, asid, start, end - 1, pstart); } + case ARMPageGetAddress: { + + + /* Check that there are enough message registers */ + assert(n_msgRegisters >= 1); + + setThreadState(ksCurThread, ThreadState_Restart); + return performPageGetAddress((void*)generic_frame_cap_get_capFBasePtr(cap)); + } + default: current_syscall_error.type = seL4_IllegalOperation; @@ -2008,6 +2019,22 @@ performPageTableInvocationUnmap(cap_t cap, cte_t *ctSlot) return EXCEPTION_NONE; } +static exception_t +performPageGetAddress(void *vbase_ptr) +{ + paddr_t capFBasePtr; + + /* Get the physical address of this frame. */ + capFBasePtr = addrFromPPtr(vbase_ptr); + + /* return it in the first message register */ + setRegister(ksCurThread, msgRegisters[0], capFBasePtr); + setRegister(ksCurThread, msgInfoRegister, + wordFromMessageInfo(message_info_new(0, 0, 0, 1))); + + return EXCEPTION_NONE; +} + static bool_t PURE pteCheckIfMapped(pte_t *pte) { diff --git a/src/arch/ia32/kernel/vspace.c b/src/arch/ia32/kernel/vspace.c index 65e3344b2..19538d576 100644 --- a/src/arch/ia32/kernel/vspace.c +++ b/src/arch/ia32/kernel/vspace.c @@ -1380,6 +1380,23 @@ static exception_t performASIDPoolInvocation(asid_t asid, asid_pool_t* poolPtr, return EXCEPTION_NONE; } +static exception_t +performPageGetAddress(void *vbase_ptr) +{ + paddr_t capFBasePtr; + + /* Get the physical address of this frame. */ + capFBasePtr = pptr_to_paddr(vbase_ptr); + + /* return it in the first message register */ + setRegister(ksCurThread, msgRegisters[0], capFBasePtr); + setRegister(ksCurThread, msgInfoRegister, + wordFromMessageInfo(message_info_new(0, 0, 0, 1))); + + return EXCEPTION_NONE; +} + + static inline bool_t checkVPAlignment(vm_page_size_t sz, word_t w) { @@ -1830,6 +1847,15 @@ decodeIA32FrameInvocation( return decodeIA32IOMapInvocation(label, length, cte, cap, extraCaps, buffer); } #endif + + case IA32PageGetAddress: { + /* Return it in the first message register. */ + assert(n_msgRegisters >= 1); + + setThreadState(ksCurThread, ThreadState_Restart); + return performPageGetAddress((void*)cap_frame_cap_get_capFBasePtr(cap)); + } + default: current_syscall_error.type = seL4_IllegalOperation; From 54cade4c32f9309f81302d7de3441a4b4cbbe02f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 18 Jul 2014 09:24:29 +0200 Subject: [PATCH 02/13] adjust LICENSE file name to header reference. --- LICENSE_GPL2.txt => LICENSE_GPLv2.txt | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename LICENSE_GPL2.txt => LICENSE_GPLv2.txt (100%) diff --git a/LICENSE_GPL2.txt b/LICENSE_GPLv2.txt similarity index 100% rename from LICENSE_GPL2.txt rename to LICENSE_GPLv2.txt From 24fa2a2998aec5f6267ec3c86d669a35ac87c83b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 18 Jul 2014 09:32:05 +0200 Subject: [PATCH 03/13] Remove logo; clean up copyright marking. --- manual/disy.sty | 16 ++++++++-------- manual/imgs/nicta-bw.pdf | Bin 5101 -> 0 bytes manual/imgs/nicta-col.pdf | Bin 5101 -> 0 bytes manual/manual.tex | 7 ++----- 4 files changed, 10 insertions(+), 13 deletions(-) delete mode 100755 manual/imgs/nicta-bw.pdf delete mode 100755 manual/imgs/nicta-col.pdf diff --git a/manual/disy.sty b/manual/disy.sty index c20fa3510..b8e95debc 100644 --- a/manual/disy.sty +++ b/manual/disy.sty @@ -67,7 +67,7 @@ \newcommand{\AuthorEmail}[1]{\def\AuthorEmailString{#1}} \newcommand{\CrestFileName}{\ifColor unicrest-colour\else unicrest-screen\fi} -\newcommand{\LogoFileName}{\ifColor nicta-col\else nicta-bw\fi} +%\newcommand{\LogoFileName}{\ifColor nicta-col\else nicta-bw\fi} \AuthorEmail{disy@cse.unsw.edu.au} \newlength{\centeroffset} @@ -93,7 +93,7 @@ %\addtolength{\ERTOSw}{-\LogoW}\addtolength{\ERTOSw}{-2em}% \settowidth{\ERTOSw}{{\sf\large http://ssrg.nicta.com.au/}}% %\settowidth{\ERTOSw}{{\sf\large Operating Systems Group}}% - \newcommand{\NICTAlogo}{\includegraphics[width=\LogoW]{imgs/\LogoFileName}}% + %\newcommand{\NICTAlogo}{\includegraphics[width=\LogoW]{imgs/\LogoFileName}}% \noindent\sf% \begin{minipage}[b]{\textwidth}\sf\large% \hspace*{-10mm}% @@ -104,12 +104,12 @@ \url{http://ssrg.nicta.com.au/}\\~ \end{minipage} \hfill - \ifx\undefined\hyperref% - \NICTAlogo% - \else% - \raisebox{2mm}{\href{http://nicta.com.au}{\NICTAlogo}}% - \fi% - \else~ +% \ifx\undefined\hyperref% +% \NICTAlogo% +% \else% +% \raisebox{2mm}{\href{http://nicta.com.au}{\NICTAlogo}}% +% \fi% +% \else~ \fi% \end{minipage}% \hspace*{-4mm}% diff --git a/manual/imgs/nicta-bw.pdf b/manual/imgs/nicta-bw.pdf deleted file mode 100755 index a50a4dff8e5a31ee5e5c13ccc600e513707a4a13..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 5101 zcmai&2{@E(_rO!ukt~ITOxf32%}~fPwydG-GG-o9V}_Z*P-IDq@=6gUlvH>n$-ZSv z$Wmk{vXc}=mgswi*Y)P_qoq~?sLw4?zyhtk+#GcC?ix*5b4^n`LU0W zzutROTL(cx;ZTa(X^4gf6lMyLJ?N*PXi#JYg&BB~=l~V`CE@7+4j@p708~p0LZedw zycdMgt7yY%BgaYzDs<9gi$52ky$zAa`UwJ%iGOK;Z%o5XYs_CHiaE!8L;SL(O@KE5 zg<0Y~Hl9>~Oow7Ox3>al6kjRpR_}tJyKw-L|htPj`2!Z__8fMen|4Ma|Lusyb zAy3n?;O@hF=hlqMLnYZV*H}+HDQx`Cp2_oLb(&q9+G3w!Q-CRYjM%}a$*L3b?sFHV z>vI?E=L&!J`JY3Ba_3)cYn8Aq3O0r8jyRBaxG*q+@%>n~1?O;5P=#A*xW()Uq+&q+ z!b07v(#BT{;zwTdR5_<6TwVe$KmA_XIa%jy@I}jV^rJYn*abIbUO{<+7}8fW_)%o2 zU_0-h9pMr|U3D<4#O_x)=QOzPvs_v?Iybm5s5nqQ{?T@g^<>5H?sIFojG`C!g4bH# z4V<)mu`V$^+nRCmyvf??!ovLG=OarHE!AMQ&j#fqMtkSK9*Cfp)8uWN{AayWm(DH) z#+~aDz}&TM_2&)X5-X3~8CW7CN|q!hkRP!tXiTORP?x!w~7!#Ih?kv zp{n_W43dbMR+xe&ZQ|B>iOb+8IKZaaYCrF39q0CJxD&-$rxMM7GsXPCK%@>M-_(Uuy|!!oAzxXW z^U?R)>pn~dWRylUuk^!ga2jFl?`S24hwtubRxNU)HSIZh7h_&CE^t>M)llLU^nONI zNQm46HJt76=$M}{uGRe^U)Hdu8dipLKP~pF)gYtCpLX^1iy-oA?Ygwuf&lsLF!A>} zC66L!n|%PGVY}MNkQP9U5Rw4V9mOg%A>QBI>oVEn<+eS}PVA+`u`kPHEy@n=&-~*8 z>I}QHnli2j3iQn1I;reE@!fQxBfw+ywB0Ctz&OPNZjF0o6*FVMyNzGVL21hLwsyj_ z-N=H5$D-m5Bby++sunhTM@#I(sO6St*{zR^EhnEW`$FppmynS48yM)Ah@Ilm0V+NVnam*TYsi zHRD&s>7uR*QI`@99x&k8`6n%N+C>cO@DS!Ovg;v2aXzBAieyr>VtG*^P1Bro3a zN=BAXNc8#HzU>zm00nF>CvCy9>62Y?Bf9ZY3A?DsB@fUC2;oAJ21H&o(7e zC=Vh!P2aQ;;}dsb0OJ)H7Q5dWPFl~H{_|_ylRb&5oiQ(kM$)a=xp%Q-KcY*YqBW-l zPxz&CZAUR0=1t%z{u8X8x95ct76PPrlHH;bSh~%8o&x%uoTB~7cRU^~PZz$O_TnIv zB&z7!zgD6i*B#V|e15^Ge#s^SQAl<(Ln;4=6vNHQ`A=Ql8#^GRw3=2x^v;Q@FpUkf zcphH;#;HcpZ#>bnVwpTj?JlKjA9wf`0aXrh6Popu;^>Pzc0I>%#ivM~wK!5H{EGh- z_UZ1dAGOs&YNBq*who=$4j9OJvEaxH5<&2+U5DC(dPo9zw@H>+v`qt-?cXTK3#(Nc(&#u zhfchkxjicF=%k}uwU-p`(9iLT_7}Qib%i{Fe{s8kSbI z4@hrFtr3oKsV2u2`=Xvz#2vJ1^WjOfezY{5Yi`{T^ca_yt0N(dPfHM=aUIuo)-+<# zcRoLgi>Q{npzIw4eJSo0?tV^XXDho<^3(}Z@dQESPKyDCM7}-#XM0`7=U!n^Gx?Pw zgN92o_fPUa-_@7Yj++XPt!{W1yUPFV4~rLZNmW2no=uxwZ{0)ZwzE>iw7bb4ayf!$pA~{JuMzGW9xyofdnz z($f$ZtKUAATdMi+h_j!_2p_+bS>oRn<*1SD;GLVG!dkKdduSI@egT2L-)!kZp#-zmDYdzLD2 zsOhmrUFL*TFv66F7VAUwI2AjJ3sgvSeiQh**(vRf41?HVd-e=d}6mU z;V5$F4C!Ty7;4~B`_*Ib55t_Ul=Mc%i&&YaY(Jqs^GD`mv6>@l@_Wp=jL&if>RyqI zN|=@i-8D2GQ(3ydFE=E3zfa)Nsi+9ipl$)*x3||7Sw^}R*ROUPmkb}}3yzHOIcDP4 z!YJzzKN~0~9t@E!?ee{)!_qr=KkCsGC6os~aBIlW07e#4h~DdONIuoO#GOdXoN{rt zbstE17_qKx>vF}p{oc{-cM_{+<9Phy_ZN-Rb0f6J#uLS$cQ{Yx9S0r@6}a*u3!8kK za$v8H63R?a{_)P{suhuV1h@_*;9o>#CqbH zIQdF}r#^EJ)`hyaeKi`wzozQO<;SadEbeSpt-#aFRR^6?%oB_iVkE6dnFB(A45~&W zlC0B`NbB-LEzpMV^Zl8gdIbU;F;r<;J0*%9q2ZOv-?g{t*HJ=O``mzpGWs`V#DwY3 z4&S8bABr_O{94jOFDlntEu`5<)YB`-^*^Cx_;F^Qns@Mu?57E*${}J{ zC&ZL3syQLK-`ep5P&ZMXv`V%snK@hlu+gFv-`uu%Mc5;g1 zvFm2^yj-gGGt>2n8*kzhvhOaO;u<@1ME^ci7CqX1H02Bt~LAdNkx+Y~RQ!*=?IqJU+u8=ev!!O2~;9L0DredeuBF z9&-(ApxOEDoo2+2R)X&^Pbm$xYEj3K7syJGPHxEgq!U?HvU49sF9qr4#*wA;kYXRB zZ8cnc*+RJnok>oS^=M$2Exi)*jq#JQ=wai# zmDI8LDS!7!RasaAxw!6hj<-bp45=95Ju2y7(25@*n&d+!iA$cjeTRxL)s}z1nhZ2d9N*@8WBm?RD>GeoAwRcZWN8F< zJhr;A`I3}z&Us6LcvYE`dG~fV z43{NO&{Hq(>@HFrlAO1!ErBB3{=Eg5TQkQ8o33Zx zsK1Y&>>d7D{Iwxc`Ig(>WRY=}V-syZ?Dp|;efqJ;frabZ{7#BYwqoKI3aN(KVmKxs zZ6Vn245vpSQK;75cmlA2ae6caRDFY}K#YUwGw6oabdX&)<_u{F2!aWUAUPV+P*4Pu zLO0%#AUkd?`WqfMbhmci#J#@_!mM?mbgJ(L4{t&3?^OGXzJ;Y36!8mLZtVDfTQ`Hk zRp3bY#^;w+%-EQVK!~*lyzx{#-IGEFfmX-d#==}*5(!6P)WN476ov!*JPClFnY{@V zv5C*lTN&LLZ*Bb-)grc#-TWa0Vo(0PVmAC{#)5`#g~#k3Y(=+uY|Q2Y?eBKMCX8di6Tqq?LErQ!zF^Y< zBy|%{A`NtZvo3z^BOre518myV!_)C3ipOT>g7#O-;+Nw2wQTjkehD+FIA$rz;SPc4 zstz758i7#7qSX}<2w6B>RvvVaLj3<#ATaO-5PbrjL+zjlxC&YYEaqdr zcq%;*3N|-3`Xmgx{4a&WpaSj?@I0`P&6;99p_|o3hHl9aC@^;$Gk?qANbqX>ONK;) zDf*WTfdFgsUosRN%)&oqC@cody91^+DvXf*t{*wARzUu1MD-jf7SH(F>L7X*O?Zv%w_Ru!{yz&{ydvO5Ke zU={^)fCH;c1C0mV;CR3t4Ir^Z3=*lT1|ZM`JO)E_S0!K(?pl!ltpeVn$-ZSv z$Wmk{vXc}=mgswi*Y)P_qoq~?sLw4?zyhtk+#GcC?ix*5b4^n`LU0W zzutROTL(cx;ZTa(X^4gf6lMyLJ?N*PXi#JYg&BB~=l~V`CE@7+4j@p708~p0LZedw zycdMgt7yY%BgaYzDs<9gi$52ky$zAa`UwJ%iGOK;Z%o5XYs_CHiaE!8L;SL(O@KE5 zg<0Y~Hl9>~Oow7Ox3>al6kjRpR_}tJyKw-L|htPj`2!Z__8fMen|4Ma|Lusyb zAy3n?;O@hF=hlqMLnYZV*H}+HDQx`Cp2_oLb(&q9+G3w!Q-CRYjM%}a$*L3b?sFHV z>vI?E=L&!J`JY3Ba_3)cYn8Aq3O0r8jyRBaxG*q+@%>n~1?O;5P=#A*xW()Uq+&q+ z!b07v(#BT{;zwTdR5_<6TwVe$KmA_XIa%jy@I}jV^rJYn*abIbUO{<+7}8fW_)%o2 zU_0-h9pMr|U3D<4#O_x)=QOzPvs_v?Iybm5s5nqQ{?T@g^<>5H?sIFojG`C!g4bH# z4V<)mu`V$^+nRCmyvf??!ovLG=OarHE!AMQ&j#fqMtkSK9*Cfp)8uWN{AayWm(DH) z#+~aDz}&TM_2&)X5-X3~8CW7CN|q!hkRP!tXiTORP?x!w~7!#Ih?kv zp{n_W43dbMR+xe&ZQ|B>iOb+8IKZaaYCrF39q0CJxD&-$rxMM7GsXPCK%@>M-_(Uuy|!!oAzxXW z^U?R)>pn~dWRylUuk^!ga2jFl?`S24hwtubRxNU)HSIZh7h_&CE^t>M)llLU^nONI zNQm46HJt76=$M}{uGRe^U)Hdu8dipLKP~pF)gYtCpLX^1iy-oA?Ygwuf&lsLF!A>} zC66L!n|%PGVY}MNkQP9U5Rw4V9mOg%A>QBI>oVEn<+eS}PVA+`u`kPHEy@n=&-~*8 z>I}QHnli2j3iQn1I;reE@!fQxBfw+ywB0Ctz&OPNZjF0o6*FVMyNzGVL21hLwsyj_ z-N=H5$D-m5Bby++sunhTM@#I(sO6St*{zR^EhnEW`$FppmynS48yM)Ah@Ilm0V+NVnam*TYsi zHRD&s>7uR*QI`@99x&k8`6n%N+C>cO@DS!Ovg;v2aXzBAieyr>VtG*^P1Bro3a zN=BAXNc8#HzU>zm00nF>CvCy9>62Y?Bf9ZY3A?DsB@fUC2;oAJ21H&o(7e zC=Vh!P2aQ;;}dsb0OJ)H7Q5dWPFl~H{_|_ylRb&5oiQ(kM$)a=xp%Q-KcY*YqBW-l zPxz&CZAUR0=1t%z{u8X8x95ct76PPrlHH;bSh~%8o&x%uoTB~7cRU^~PZz$O_TnIv zB&z7!zgD6i*B#V|e15^Ge#s^SQAl<(Ln;4=6vNHQ`A=Ql8#^GRw3=2x^v;Q@FpUkf zcphH;#;HcpZ#>bnVwpTj?JlKjA9wf`0aXrh6Popu;^>Pzc0I>%#ivM~wK!5H{EGh- z_UZ1dAGOs&YNBq*who=$4j9OJvEaxH5<&2+U5DC(dPo9zw@H>+v`qt-?cXTK3#(Nc(&#u zhfchkxjicF=%k}uwU-p`(9iLT_7}Qib%i{Fe{s8kSbI z4@hrFtr3oKsV2u2`=Xvz#2vJ1^WjOfezY{5Yi`{T^ca_yt0N(dPfHM=aUIuo)-+<# zcRoLgi>Q{npzIw4eJSo0?tV^XXDho<^3(}Z@dQESPKyDCM7}-#XM0`7=U!n^Gx?Pw zgN92o_fPUa-_@7Yj++XPt!{W1yUPFV4~rLZNmW2no=uxwZ{0)ZwzE>iw7bb4ayf!$pA~{JuMzGW9xyofdnz z($f$ZtKUAATdMi+h_j!_2p_+bS>oRn<*1SD;GLVG!dkKdduSI@egT2L-)!kZp#-zmDYdzLD2 zsOhmrUFL*TFv66F7VAUwI2AjJ3sgvSeiQh**(vRf41?HVd-e=d}6mU z;V5$F4C!Ty7;4~B`_*Ib55t_Ul=Mc%i&&YaY(Jqs^GD`mv6>@l@_Wp=jL&if>RyqI zN|=@i-8D2GQ(3ydFE=E3zfa)Nsi+9ipl$)*x3||7Sw^}R*ROUPmkb}}3yzHOIcDP4 z!YJzzKN~0~9t@E!?ee{)!_qr=KkCsGC6os~aBIlW07e#4h~DdONIuoO#GOdXoN{rt zbstE17_qKx>vF}p{oc{-cM_{+<9Phy_ZN-Rb0f6J#uLS$cQ{Yx9S0r@6}a*u3!8kK za$v8H63R?a{_)P{suhuV1h@_*;9o>#CqbH zIQdF}r#^EJ)`hyaeKi`wzozQO<;SadEbeSpt-#aFRR^6?%oB_iVkE6dnFB(A45~&W zlC0B`NbB-LEzpMV^Zl8gdIbU;F;r<;J0*%9q2ZOv-?g{t*HJ=O``mzpGWs`V#DwY3 z4&S8bABr_O{94jOFDlntEu`5<)YB`-^*^Cx_;F^Qns@Mu?57E*${}J{ zC&ZL3syQLK-`ep5P&ZMXv`V%snK@hlu+gFv-`uu%Mc5;g1 zvFm2^yj-gGGt>2n8*kzhvhOaO;u<@1ME^ci7CqX1H02Bt~LAdNkx+Y~RQ!*=?IqJU+u8=ev!!O2~;9L0DredeuBF z9&-(ApxOEDoo2+2R)X&^Pbm$xYEj3K7syJGPHxEgq!U?HvU49sF9qr4#*wA;kYXRB zZ8cnc*+RJnok>oS^=M$2Exi)*jq#JQ=wai# zmDI8LDS!7!RasaAxw!6hj<-bp45=95Ju2y7(25@*n&d+!iA$cjeTRxL)s}z1nhZ2d9N*@8WBm?RD>GeoAwRcZWN8F< zJhr;A`I3}z&Us6LcvYE`dG~fV z43{NO&{Hq(>@HFrlAO1!ErBB3{=Eg5TQkQ8o33Zx zsK1Y&>>d7D{Iwxc`Ig(>WRY=}V-syZ?Dp|;efqJ;frabZ{7#BYwqoKI3aN(KVmKxs zZ6Vn245vpSQK;75cmlA2ae6caRDFY}K#YUwGw6oabdX&)<_u{F2!aWUAUPV+P*4Pu zLO0%#AUkd?`WqfMbhmci#J#@_!mM?mbgJ(L4{t&3?^OGXzJ;Y36!8mLZtVDfTQ`Hk zRp3bY#^;w+%-EQVK!~*lyzx{#-IGEFfmX-d#==}*5(!6P)WN476ov!*JPClFnY{@V zv5C*lTN&LLZ*Bb-)grc#-TWa0Vo(0PVmAC{#)5`#g~#k3Y(=+uY|Q2Y?eBKMCX8di6Tqq?LErQ!zF^Y< zBy|%{A`NtZvo3z^BOre518myV!_)C3ipOT>g7#O-;+Nw2wQTjkehD+FIA$rz;SPc4 zstz758i7#7qSX}<2w6B>RvvVaLj3<#ATaO-5PbrjL+zjlxC&YYEaqdr zcq%;*3N|-3`Xmgx{4a&WpaSj?@I0`P&6;99p_|o3hHl9aC@^;$Gk?qANbqX>ONK;) zDf*WTfdFgsUosRN%)&oqC@cody91^+DvXf*t{*wARzUu1MD-jf7SH(F>L7X*O?Zv%w_Ru!{yz&{ydvO5Ke zU={^)fCH;c1C0mV;CR3t4Ir^Z3=*lT1|ZM`JO)E_S0!K(?pl!ltpeV Date: Fri, 18 Jul 2014 17:46:59 +0200 Subject: [PATCH 04/13] add getpaddr changes to haskell (by Joel Beeren) --- haskell/src/SEL4/API/Invocation.lhs | 1 + haskell/src/SEL4/API/Invocation/ARM.lhs | 2 ++ haskell/src/SEL4/Kernel/VSpace/ARM.lhs | 12 ++++++++++++ haskell/src/SEL4/Machine/Hardware/ARM.lhs | 3 +++ 4 files changed, 18 insertions(+) diff --git a/haskell/src/SEL4/API/Invocation.lhs b/haskell/src/SEL4/API/Invocation.lhs index d82640711..c0932804d 100644 --- a/haskell/src/SEL4/API/Invocation.lhs +++ b/haskell/src/SEL4/API/Invocation.lhs @@ -186,6 +186,7 @@ This datatype is defined globally over architectures as well as object types. > | ARMPageInvalidate_Data > | ARMPageCleanInvalidate_Data > | ARMPageUnify_Instruction +> | ARMPageGetAddress > | ARMASIDControlMakePool > | ARMASIDPoolAssign > deriving (Enum, Bounded, Eq) diff --git a/haskell/src/SEL4/API/Invocation/ARM.lhs b/haskell/src/SEL4/API/Invocation/ARM.lhs index 399da013e..d64988838 100644 --- a/haskell/src/SEL4/API/Invocation/ARM.lhs +++ b/haskell/src/SEL4/API/Invocation/ARM.lhs @@ -80,6 +80,8 @@ There are five ARM-specific object types; however, only four of them may be invo > pageFlushPStart :: PAddr, > pageFlushPD :: PPtr PDE, > pageFlushASID :: ASID } +> | PageGetAddr { +> pageGetBasePtr :: PPtr Word } > deriving Show > data FlushType diff --git a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs index af72697d0..f8b882005 100644 --- a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs +++ b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs @@ -1139,6 +1139,7 @@ Virtual page capabilities may each represent a single mapping into a page table. > (ARMPageInvalidate_Data, _, _) -> decodeARMPageFlush label args cap > (ARMPageCleanInvalidate_Data, _, _) -> decodeARMPageFlush label args cap > (ARMPageUnify_Instruction, _, _) -> decodeARMPageFlush label args cap +> (ARMPageGetAddress, _, _) -> return $ InvokePage $ PageGetAddr (capVPBasePtr cap) > _ -> throw IllegalOperation @@ -1326,6 +1327,17 @@ Don't flush an empty range. > when root_switched $ do > tcb <- getCurThread > setVMRoot tcb +> +> performPageInvocation (PageGetAddr ptr) = do +> let paddr = fromPAddr $ addrFromPPtr ptr +> ct <- getCurThread +> msgTransferred <- setMRs ct Nothing [paddr] +> msgInfo <- return $ MI { +> msgLength = msgTransferred, +> msgExtraCaps = 0, +> msgCapsUnwrapped = 0, +> msgLabel = 0 } +> setMessageInfo ct msgInfo > performASIDControlInvocation :: ASIDControlInvocation -> Kernel () > performASIDControlInvocation (MakePool frame slot parent base) = do diff --git a/haskell/src/SEL4/Machine/Hardware/ARM.lhs b/haskell/src/SEL4/Machine/Hardware/ARM.lhs index 1eb76460e..48e7e0dc8 100644 --- a/haskell/src/SEL4/Machine/Hardware/ARM.lhs +++ b/haskell/src/SEL4/Machine/Hardware/ARM.lhs @@ -80,6 +80,9 @@ The ARM MMU does not allow access to physical addresses while translation is ena > addrFromPPtr :: PPtr a -> PAddr > addrFromPPtr = Platform.addrFromPPtr +> fromPAddr :: PAddr -> Word +> fromPAddr = Platform.fromPAddr + \subsection{Hardware Access} The following functions define the ARM-specific interface between the kernel and the hardware. Most of them depend on the simulator in use, and are therefore defined in the platform module. From 1d0b002548e229a6cc83d02d21b887fdc4d88322 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 18 Jul 2014 18:04:45 +0200 Subject: [PATCH 05/13] Sync Haskell code with C --- haskell/src/SEL4/API/Invocation/ARM.lhs | 2 ++ haskell/src/SEL4/Kernel/VSpace/ARM.lhs | 35 +++++++++++++++++++++---- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/haskell/src/SEL4/API/Invocation/ARM.lhs b/haskell/src/SEL4/API/Invocation/ARM.lhs index d64988838..ed5c1defd 100644 --- a/haskell/src/SEL4/API/Invocation/ARM.lhs +++ b/haskell/src/SEL4/API/Invocation/ARM.lhs @@ -65,10 +65,12 @@ There are five ARM-specific object types; however, only four of them may be invo > -- FIXME: should we consolidate start, end into a tuple > data PageInvocation > = PageMap { +> pageMapASID :: ASID, > pageMapCap :: Capability, > pageMapCTSlot :: PPtr CTE, > pageMapEntries :: Either (PTE, [PPtr PTE]) (PDE, [PPtr PDE]) } > | PageRemap { +> pageRemapASID :: ASID, > pageRemapEntries :: Either (PTE, [PPtr PTE]) (PDE, [PPtr PDE]) } > | PageUnmap { > pageUnmapCap :: ArchCapability, diff --git a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs index f8b882005..19e35a715 100644 --- a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs +++ b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs @@ -1106,6 +1106,7 @@ Virtual page capabilities may each represent a single mapping into a page table. > (attribsFromWord attr) pd > ensureSafeMapping entries > return $ InvokePage $ PageMap { +> pageMapASID = asid, > pageMapCap = ArchObjectCap $ > cap { capVPMappedAddress = Just (asid, VPtr vaddr) }, > pageMapCTSlot = cte, @@ -1130,6 +1131,7 @@ Virtual page capabilities may each represent a single mapping into a page table. > vaddr (capVPSize cap) vmRights (attribsFromWord attr) pd > ensureSafeMapping entries > return $ InvokePage $ PageRemap { +> pageRemapASID = asidCheck, > pageRemapEntries = entries } > (ARMPageRemap, _, _) -> throw TruncatedMessage > (ARMPageUnmap, _, _) -> return $ InvokePage $ PageUnmap { @@ -1280,36 +1282,59 @@ Don't flush an empty range. > updateCap ctSlot (ArchObjectCap $ > cap { capPTMappedAddress = Nothing }) +When checking if there was already something mapped before a PageMap or PageRemap, +we need only check the first slot because ensureSafeMapping tells us that +the PT/PD is consistent. + +> pteCheckIfMapped :: PPtr PTE -> Kernel Bool +> pteCheckIfMapped slot = do +> pt <- getObject slot +> return $ pt /= InvalidPTE + +> pdeCheckIfMapped :: PPtr PDE -> Kernel Bool +> pdeCheckIfMapped slot = do +> pd <- getObject slot +> return $ pd /= InvalidPDE + > performPageInvocation :: PageInvocation -> Kernel () > -> performPageInvocation (PageMap cap ctSlot entries) = do +> performPageInvocation (PageMap asid cap ctSlot entries) = do > updateCap ctSlot cap > case entries of > Left (pte, slots) -> do +> tlbFlush <- pteCheckIfMapped (head slots) > mapM (flip storePTE pte) slots > doMachineOp $ > cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) > (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PTE)) - 1)) > (addrFromPPtr (head slots)) +> when tlbFlush $ invalidateTLBByASID asid > Right (pde, slots) -> do +> tlbFlush <- pdeCheckIfMapped (head slots) > mapM (flip storePDE pde) slots > doMachineOp $ > cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) > (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PDE)) - 1)) > (addrFromPPtr (head slots)) +> when tlbFlush $ invalidateTLBByASID asid > -> performPageInvocation (PageRemap (Left (pte, slots))) = do -> mapM_ (flip storePTE pte) slots +> performPageInvocation (PageRemap asid (Left (pte, slots))) = do +> tlbFlush <- pteCheckIfMapped (head slots) +> mapM (flip storePTE pte) slots > doMachineOp $ > cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) > (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PTE)) - 1)) > (addrFromPPtr (head slots)) -> performPageInvocation (PageRemap (Right (pde, slots))) = do -> mapM_ (flip storePDE pde) slots +> when tlbFlush $ invalidateTLBByASID asid +> +> performPageInvocation (PageRemap asid (Right (pde, slots))) = do +> tlbFlush <- pdeCheckIfMapped (head slots) +> mapM (flip storePDE pde) slots > doMachineOp $ > cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots) > (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PDE)) - 1)) > (addrFromPPtr (head slots)) +> when tlbFlush $ invalidateTLBByASID asid > > performPageInvocation (PageUnmap cap ctSlot) = do > case capVPMappedAddress cap of From 2a5504b3f0932327bec758197e667715d35ed33c Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 19 Jul 2014 10:11:41 +0200 Subject: [PATCH 06/13] removed ancient arch tags --- haskell/SEL4.cabal | 1 - haskell/Setup.hs | 1 - haskell/doc/Makefile | 1 - haskell/doc/figures/clientkernel.mp | 2 +- haskell/doc/figures/clientserver.mp | 2 +- haskell/doc/figures/derive.mp | 2 +- haskell/doc/figures/ipctransfer.mp | 2 +- haskell/doc/figures/modules.dot | 2 -- haskell/doc/figures/truncation.mp | 2 +- haskell/doc/haskell.tex | 2 +- haskell/doc/lambdaTeX.sty | 2 +- haskell/doc/mkfunctions.pl | 1 - haskell/doc/mkmodulesgraph.pl | 1 - haskell/doc/overview.tex | 2 +- haskell/doc/packages | 1 - haskell/doc/pubs.bib | 2 +- haskell/doc/refman.tex | 2 +- haskell/mkhsboot.pl | 1 - haskell/src/Data/BinaryTree.hs | 1 - haskell/src/Data/Helpers.hs | 1 - haskell/src/HaskellCPU.lhs | 2 +- haskell/src/SEL4.lhs | 2 +- haskell/src/SEL4/API.lhs | 2 +- haskell/src/SEL4/API/Failures.lhs | 2 +- haskell/src/SEL4/API/Invocation.lhs | 2 +- haskell/src/SEL4/API/Invocation/ARM.lhs | 2 +- haskell/src/SEL4/API/Syscall.lhs | 2 +- haskell/src/SEL4/API/Types.lhs | 2 +- haskell/src/SEL4/API/Types/ARM.lhs | 2 +- haskell/src/SEL4/API/Types/HaskellCPU.lhs | 2 +- haskell/src/SEL4/API/Types/Universal.lhs | 2 +- haskell/src/SEL4/Kernel.lhs | 2 +- haskell/src/SEL4/Kernel/CSpace.lhs | 2 +- haskell/src/SEL4/Kernel/FaultHandler.lhs | 2 +- haskell/src/SEL4/Kernel/Init.lhs | 2 +- haskell/src/SEL4/Kernel/Thread.lhs | 2 +- haskell/src/SEL4/Kernel/VSpace/ARM.lhs | 2 +- haskell/src/SEL4/Kernel/VSpace/CSpace.lhs | 2 +- haskell/src/SEL4/Kernel/VSpace/HaskellCPU.lhs | 2 +- haskell/src/SEL4/Machine.lhs | 2 +- haskell/src/SEL4/Machine/Hardware.lhs | 2 +- haskell/src/SEL4/Machine/Hardware/ARM.lhs | 2 +- haskell/src/SEL4/Machine/Hardware/ARM/QEmu.hs | 1 - haskell/src/SEL4/Machine/Hardware/Alpha.lhs | 2 +- haskell/src/SEL4/Machine/Hardware/HaskellCPU.lhs | 2 +- haskell/src/SEL4/Machine/RegisterSet.lhs | 2 +- haskell/src/SEL4/Machine/RegisterSet/ARM.lhs | 2 +- haskell/src/SEL4/Machine/RegisterSet/HaskellCPU.lhs | 2 +- haskell/src/SEL4/Model.lhs | 2 +- haskell/src/SEL4/Model/Failures.lhs | 2 +- haskell/src/SEL4/Model/PSpace.lhs | 2 +- haskell/src/SEL4/Model/Preemption.lhs | 2 +- haskell/src/SEL4/Model/StateData.lhs | 2 +- haskell/src/SEL4/Model/Syscall.lhs | 2 +- haskell/src/SEL4/Object.lhs | 2 +- haskell/src/SEL4/Object/AsyncEndpoint.lhs | 2 +- haskell/src/SEL4/Object/CNode.lhs | 2 +- haskell/src/SEL4/Object/Endpoint.lhs | 2 +- haskell/src/SEL4/Object/Instances.lhs | 2 +- haskell/src/SEL4/Object/Interrupt.lhs | 2 +- haskell/src/SEL4/Object/Interrupt/ARM.lhs | 2 +- haskell/src/SEL4/Object/ObjectType.lhs | 2 +- haskell/src/SEL4/Object/ObjectType/ARM.lhs | 2 +- haskell/src/SEL4/Object/ObjectType/HaskellCPU.lhs | 2 +- haskell/src/SEL4/Object/Structures.lhs | 2 +- haskell/src/SEL4/Object/Structures/ARM.lhs | 2 +- haskell/src/SEL4/Object/TCB.lhs | 2 +- 67 files changed, 56 insertions(+), 68 deletions(-) diff --git a/haskell/SEL4.cabal b/haskell/SEL4.cabal index db60d63fc..b7857bb93 100644 --- a/haskell/SEL4.cabal +++ b/haskell/SEL4.cabal @@ -80,4 +80,3 @@ Library -fno-warn-unrecognised-pragmas -fno-warn-unused-binds --- arch-tag: 65000561-3741-489c-91b4-ac5e8307447e diff --git a/haskell/Setup.hs b/haskell/Setup.hs index 37481e0b4..1dfbe4bab 100644 --- a/haskell/Setup.hs +++ b/haskell/Setup.hs @@ -138,5 +138,4 @@ generateHSBoot = mapM_ generateHSBoot' bootFiles ++ n ++ "-boot") unless (r == ExitSuccess) $ error "Couldn't generate boot file" --- arch-tag: df8db3ce-f891-4526-aff0-b7a3cf5036c4 diff --git a/haskell/doc/Makefile b/haskell/doc/Makefile index 99868b2d6..ae5add102 100644 --- a/haskell/doc/Makefile +++ b/haskell/doc/Makefile @@ -54,4 +54,3 @@ clean: rm -f *.aux *.toc *.bbl *.blg *.dvi *.log *.out \ figures/*.mps figures/*.pdf figures/*.log ${Target} -# arch-tag: b2d385a6-aa7d-4404-86e2-722e2adc58cd diff --git a/haskell/doc/figures/clientkernel.mp b/haskell/doc/figures/clientkernel.mp index 55e22950c..a62614934 100644 --- a/haskell/doc/figures/clientkernel.mp +++ b/haskell/doc/figures/clientkernel.mp @@ -64,4 +64,4 @@ drawarrow sw.c..res{left} cutbefore bpath.sw dashed evenly; endfig; end. -% arch-tag: b1d4e84c-e4ec-4eb0-855f-0fb671f6b721 + diff --git a/haskell/doc/figures/clientserver.mp b/haskell/doc/figures/clientserver.mp index 4f4079c1f..7ec574280 100644 --- a/haskell/doc/figures/clientserver.mp +++ b/haskell/doc/figures/clientserver.mp @@ -74,4 +74,4 @@ drawarrow op.s -- send.c cutafter bpath.send dashed evenly; endfig; end. -% arch-tag: 97d20db6-2567-4832-94e7-9da3534b94b8 + diff --git a/haskell/doc/figures/derive.mp b/haskell/doc/figures/derive.mp index db8de6198..62f57f7d5 100644 --- a/haskell/doc/figures/derive.mp +++ b/haskell/doc/figures/derive.mp @@ -54,4 +54,4 @@ draw tb.e--tn.w dashed withdots; endfig; end. -% arch-tag: 9387a596-c5ed-494c-8879-c10837f00f03 + diff --git a/haskell/doc/figures/ipctransfer.mp b/haskell/doc/figures/ipctransfer.mp index 90639a675..770e4b5c8 100644 --- a/haskell/doc/figures/ipctransfer.mp +++ b/haskell/doc/figures/ipctransfer.mp @@ -101,4 +101,4 @@ drawarrow(mrs.se -- rd.w) dashed evenly; endfig; end. -% arch-tag: f90d58c9-32b3-46cb-b9ce-3ba761ba5fe9 + diff --git a/haskell/doc/figures/modules.dot b/haskell/doc/figures/modules.dot index a8ff8704f..425d999f2 100644 --- a/haskell/doc/figures/modules.dot +++ b/haskell/doc/figures/modules.dot @@ -29,5 +29,3 @@ digraph modules { objtypes [label=Types]; Object -> objtypes; Object -> Untyped; } - -// arch-tag: 626b173f-3ee0-4d62-9744-eef2715af924 diff --git a/haskell/doc/figures/truncation.mp b/haskell/doc/figures/truncation.mp index 77c073440..c9a41c88a 100644 --- a/haskell/doc/figures/truncation.mp +++ b/haskell/doc/figures/truncation.mp @@ -40,4 +40,4 @@ drawarrow(shmrs.e -- rhmrs.w) dashed evenly; endfig; end. -% arch-tag: 7fa4aace-a858-473e-b3e5-54114cd6194b + diff --git a/haskell/doc/haskell.tex b/haskell/doc/haskell.tex index 1851dc5bc..0939181a0 100644 --- a/haskell/doc/haskell.tex +++ b/haskell/doc/haskell.tex @@ -126,4 +126,4 @@ The Haskell code presented in this document is \emph{literate Haskell}; it can b Some of the Haskell code is omitted for clarity. In particular, we omit most "import" statements (other than those which are qualified with local module names), compiler directives, and preprocessor directives. We also omit some modules that implement the interface between the kernel model and the external user-level simulators. -% arch-tag: 22cb2f60-c0a2-47c5-87ba-dc1224f9c075 + diff --git a/haskell/doc/lambdaTeX.sty b/haskell/doc/lambdaTeX.sty index 996ff72eb..1560c142b 100644 --- a/haskell/doc/lambdaTeX.sty +++ b/haskell/doc/lambdaTeX.sty @@ -1497,4 +1497,4 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% THE END %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% arch-tag: B0DCC4EB-ABF6-11D9-82F1-000393DEF6D6 + diff --git a/haskell/doc/mkfunctions.pl b/haskell/doc/mkfunctions.pl index 363d7f72c..e66d79b67 100644 --- a/haskell/doc/mkfunctions.pl +++ b/haskell/doc/mkfunctions.pl @@ -61,4 +61,3 @@ foreach $source (@lhsfiles) { close OUT; -# arch-tag: d9a9eb7c-748b-433e-b802-5576223cc336 diff --git a/haskell/doc/mkmodulesgraph.pl b/haskell/doc/mkmodulesgraph.pl index f97baa9ab..0525a4434 100644 --- a/haskell/doc/mkmodulesgraph.pl +++ b/haskell/doc/mkmodulesgraph.pl @@ -68,4 +68,3 @@ foreach $source (@lhsfiles) { print "}\n"; -# arch-tag: 5a41c5c3-7b6f-4d75-80ee-488342b7973a diff --git a/haskell/doc/overview.tex b/haskell/doc/overview.tex index a3f0d0c15..4adf76328 100644 --- a/haskell/doc/overview.tex +++ b/haskell/doc/overview.tex @@ -577,4 +577,4 @@ delivery via asynchronous IPC to a specified endpoint. This may be complemented or replaced by a callback-based delivery model in future versions or real-hardware implementations. -% arch-tag: 81b78ea5-309f-4aa5-bfed-b5d489c36d33 + diff --git a/haskell/doc/packages b/haskell/doc/packages index 5c1574bc9..95fb33723 100644 --- a/haskell/doc/packages +++ b/haskell/doc/packages @@ -18,4 +18,3 @@ dft/TeX/nicta/images ertos@nicta.com.au--private/images--nicta-logos ### include if you want ERTOS bib dft/BibTeX ertos@nicta.com.au--private/bibtex--ertos -# arch-tag: CAD0D30E-BB79-4386-8060-60E2BA51FD4B diff --git a/haskell/doc/pubs.bib b/haskell/doc/pubs.bib index a8c1a9686..2ffe12233 100644 --- a/haskell/doc/pubs.bib +++ b/haskell/doc/pubs.bib @@ -73,4 +73,4 @@ howpublished = {\url{http://www.haskell.org/tutorial/}} } -% arch-tag: 9CCD48D6-C1ED-11D9-A942-000393DEF6D6 + diff --git a/haskell/doc/refman.tex b/haskell/doc/refman.tex index 1694c6656..725a31556 100644 --- a/haskell/doc/refman.tex +++ b/haskell/doc/refman.tex @@ -302,4 +302,4 @@ This chapter defines a language and interpreter that may be used for writing sim \end{document} -% arch-tag: 5B7117E0-AB6D-11D9-ABCA-000393DEF6D6 + diff --git a/haskell/mkhsboot.pl b/haskell/mkhsboot.pl index 0eff327aa..0fbdf04e7 100644 --- a/haskell/mkhsboot.pl +++ b/haskell/mkhsboot.pl @@ -73,4 +73,3 @@ while($exports =~ / ([a-z][a-zA-Z0-9']*)/g) { } } -# arch-tag: D4C153F6-9E5E-11D9-99C4-000393DEF6D6 diff --git a/haskell/src/Data/BinaryTree.hs b/haskell/src/Data/BinaryTree.hs index 0da9ce5bc..dba08aa22 100644 --- a/haskell/src/Data/BinaryTree.hs +++ b/haskell/src/Data/BinaryTree.hs @@ -82,4 +82,3 @@ flatten :: BinaryTree a -> BinaryTree a flatten (Node Empty Empty) = Empty flatten t = t --- arch-tag: 3f1c974e-fce2-47ba-a67a-56b1b7653a3b diff --git a/haskell/src/Data/Helpers.hs b/haskell/src/Data/Helpers.hs index 6d7952aa6..ec4b4f8d9 100644 --- a/haskell/src/Data/Helpers.hs +++ b/haskell/src/Data/Helpers.hs @@ -18,4 +18,3 @@ funPartialArray f b = listArray b $ (map f) $ range b funArray :: (Ix i, Bounded i) => (i -> a) -> Array i a funArray f = funPartialArray f (minBound, maxBound) --- arch-tag: 3f1c974e-fce2-47ba-a67a-56b1b7653a3b diff --git a/haskell/src/HaskellCPU.lhs b/haskell/src/HaskellCPU.lhs index d342272b6..b0e986bb9 100644 --- a/haskell/src/HaskellCPU.lhs +++ b/haskell/src/HaskellCPU.lhs @@ -205,4 +205,4 @@ > formatError ('%':chars) (i:values) = (show i) ++ (formatError chars values) > formatError (x:chars) values = x : (formatError chars values) -% arch-tag: c5895daa-fa6e-4ba4-a4ae-51527dca5982 + diff --git a/haskell/src/SEL4.lhs b/haskell/src/SEL4.lhs index 48c624f1f..6687f69f6 100644 --- a/haskell/src/SEL4.lhs +++ b/haskell/src/SEL4.lhs @@ -59,4 +59,4 @@ The following two functions save and restore the user-level context of the curre > thread <- getCurThread > asUser thread get -% arch-tag: cecfd754-d338-4907-980b-979ae98d03c1 + diff --git a/haskell/src/SEL4/API.lhs b/haskell/src/SEL4/API.lhs index cc5ed0aca..e14b1e7f6 100644 --- a/haskell/src/SEL4/API.lhs +++ b/haskell/src/SEL4/API.lhs @@ -21,4 +21,4 @@ > import SEL4.API.Invocation > import SEL4.API.Syscall -% arch-tag: 7b4d3103-7f02-4d80-8848-2de5469c3657 + diff --git a/haskell/src/SEL4/API/Failures.lhs b/haskell/src/SEL4/API/Failures.lhs index e93d80ecc..56e6d010b 100644 --- a/haskell/src/SEL4/API/Failures.lhs +++ b/haskell/src/SEL4/API/Failures.lhs @@ -143,4 +143,4 @@ Faults and system call errors may both be caused by a failed address space looku > msgFromLookupFailure (GuardMismatch bl g gs) = > [4, fromIntegral bl, g, fromIntegral gs] -% arch-tag: af70a6ed-db97-4179-92ae-cc78155f67b4 + diff --git a/haskell/src/SEL4/API/Invocation.lhs b/haskell/src/SEL4/API/Invocation.lhs index c0932804d..2b6447012 100644 --- a/haskell/src/SEL4/API/Invocation.lhs +++ b/haskell/src/SEL4/API/Invocation.lhs @@ -215,4 +215,4 @@ Decode the invocation type requested by a particular message label. > ARMPageUnify_Instruction -> True > _ -> False -% arch-tag: DF38ABBD-0D6E-4996-8E5B-42FC4E54CFA9 + diff --git a/haskell/src/SEL4/API/Invocation/ARM.lhs b/haskell/src/SEL4/API/Invocation/ARM.lhs index ed5c1defd..702c91cd5 100644 --- a/haskell/src/SEL4/API/Invocation/ARM.lhs +++ b/haskell/src/SEL4/API/Invocation/ARM.lhs @@ -119,4 +119,4 @@ The ARM platform currently does not define any additional register sets for the > data CopyRegisterSets = ARMNoExtraRegisters > deriving Show -% arch-tag: EA7C9D75-7DCC-4904-906D-CCC1E6B7B020 + diff --git a/haskell/src/SEL4/API/Syscall.lhs b/haskell/src/SEL4/API/Syscall.lhs index 76539f02f..935ad802c 100644 --- a/haskell/src/SEL4/API/Syscall.lhs +++ b/haskell/src/SEL4/API/Syscall.lhs @@ -253,4 +253,4 @@ While the system call is running, the thread's state is set to "Restart", so any > setThreadState Running thread > _ -> return ()) -% arch-tag: 8C5834E4-4D93-11D9-80D3-000393DEF6D6 + diff --git a/haskell/src/SEL4/API/Types.lhs b/haskell/src/SEL4/API/Types.lhs index 620412b35..0fc6d621d 100644 --- a/haskell/src/SEL4/API/Types.lhs +++ b/haskell/src/SEL4/API/Types.lhs @@ -285,4 +285,4 @@ Regions of any of the types below only appear in "BRNodeL2" regions. > deriving (Show, Enum) -% arch-tag: 8C5AB258-4D93-11D9-A85D-000393DEF6D6 + diff --git a/haskell/src/SEL4/API/Types/ARM.lhs b/haskell/src/SEL4/API/Types/ARM.lhs index 770466723..fc9bf82d7 100644 --- a/haskell/src/SEL4/API/Types/ARM.lhs +++ b/haskell/src/SEL4/API/Types/ARM.lhs @@ -68,4 +68,4 @@ There are three ARM-specific object types: virtual pages, page tables, and page > getObjectSize PageDirectoryObject _ = pdBits > getObjectSize (APIObjectType apiObjectType) size = apiGetObjectSize apiObjectType size -% arch-tag: fd7d859b-4a4d-4601-a96c-dad4a60069dd + diff --git a/haskell/src/SEL4/API/Types/HaskellCPU.lhs b/haskell/src/SEL4/API/Types/HaskellCPU.lhs index 71a8f96e9..8f31fd059 100644 --- a/haskell/src/SEL4/API/Types/HaskellCPU.lhs +++ b/haskell/src/SEL4/API/Types/HaskellCPU.lhs @@ -14,4 +14,4 @@ This module contains an instance of the machine-specific kernel API for the Hask > import SEL4.API.Types.Universal -% arch-tag: c95a5990-a310-4c01-96a1-2caef0d1a11b + diff --git a/haskell/src/SEL4/API/Types/Universal.lhs b/haskell/src/SEL4/API/Types/Universal.lhs index 07af3fa8b..90f55291b 100644 --- a/haskell/src/SEL4/API/Types/Universal.lhs +++ b/haskell/src/SEL4/API/Types/Universal.lhs @@ -46,4 +46,4 @@ The following is the definition of the five object types that are always availab > apiGetObjectSize CapTableObject size = cteSizeBits + size -% arch-tag: f244aef3-c45a-4efb-b0d6-6c885e50ee7e + diff --git a/haskell/src/SEL4/Kernel.lhs b/haskell/src/SEL4/Kernel.lhs index 587024ac2..a4963c691 100644 --- a/haskell/src/SEL4/Kernel.lhs +++ b/haskell/src/SEL4/Kernel.lhs @@ -22,4 +22,4 @@ > import SEL4.Kernel.CSpace > import SEL4.Kernel.VSpace -% arch-tag: 971fedab-35c2-44f7-ac76-6507b6af83a4 + diff --git a/haskell/src/SEL4/Kernel/CSpace.lhs b/haskell/src/SEL4/Kernel/CSpace.lhs index 7ad7b73e3..eee8283a1 100644 --- a/haskell/src/SEL4/Kernel/CSpace.lhs +++ b/haskell/src/SEL4/Kernel/CSpace.lhs @@ -190,4 +190,4 @@ The following definition will be used if the top level CNode is not valid. > resolveAddressBits _ _ _ = throw InvalidRoot -% arch-tag: a18994eb-4d18-46c5-b384-60acdb9d91cf + diff --git a/haskell/src/SEL4/Kernel/FaultHandler.lhs b/haskell/src/SEL4/Kernel/FaultHandler.lhs index 1099eecc4..2409ff9ca 100644 --- a/haskell/src/SEL4/Kernel/FaultHandler.lhs +++ b/haskell/src/SEL4/Kernel/FaultHandler.lhs @@ -83,4 +83,4 @@ If a fault IPC cannot be sent because the fault handler endpoint capability is m > ++ "\nat address " ++ (show faultPC) > doMachineOp $ debugPrint errmsg -% arch-tag: 4790525E-5E0A-11D9-BCED-000393DEF6D6 + diff --git a/haskell/src/SEL4/Kernel/Init.lhs b/haskell/src/SEL4/Kernel/Init.lhs index cdbddf26e..3e9199879 100644 --- a/haskell/src/SEL4/Kernel/Init.lhs +++ b/haskell/src/SEL4/Kernel/Init.lhs @@ -695,4 +695,4 @@ Various functions in this module use "rangesBy" to split a sorted list into cont > isAligned :: (Num a, Bits a) => a -> Int -> Bool > isAligned x n = x .&. mask n == 0 -% arch-tag: 8E06EFB3-5FA2-11D9-8AF8-000393DEF6D6 + diff --git a/haskell/src/SEL4/Kernel/Thread.lhs b/haskell/src/SEL4/Kernel/Thread.lhs index 421fe1cbc..d5fd6b0ba 100644 --- a/haskell/src/SEL4/Kernel/Thread.lhs +++ b/haskell/src/SEL4/Kernel/Thread.lhs @@ -552,4 +552,4 @@ If there is more than one security domain and the domain timeslice has expired, > when (domainTime == 0) $ rescheduleRequired % -% arch-tag: D8D60B52-5491-11D9-905A-000393DEF6D6 + diff --git a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs index 19e35a715..7cf25c0fb 100644 --- a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs +++ b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs @@ -1402,4 +1402,4 @@ The kernel model's ARM targets use an external simulation of the physical addres > setObject slot pte > doMachineOp $ storeWordVM (PPtr $ fromPPtr slot) $ wordFromPTE pte -% arch-tag: 288d2398-c68c-4e33-ba29-94ef0bab3e3a + diff --git a/haskell/src/SEL4/Kernel/VSpace/CSpace.lhs b/haskell/src/SEL4/Kernel/VSpace/CSpace.lhs index 06a44b548..54a405a0d 100644 --- a/haskell/src/SEL4/Kernel/VSpace/CSpace.lhs +++ b/haskell/src/SEL4/Kernel/VSpace/CSpace.lhs @@ -83,4 +83,4 @@ This module contains definitions of the VSpace functions for platforms that do n > Nothing -> fail "Couldn't find appropriate size for device" > return $ FrameCap wptr (pageBitsForSize size) True True -% arch-tag: 4dfc18a3-24ab-47cf-b109-4455770f4de9 + diff --git a/haskell/src/SEL4/Kernel/VSpace/HaskellCPU.lhs b/haskell/src/SEL4/Kernel/VSpace/HaskellCPU.lhs index 29a21a2c4..a1aeba3bb 100644 --- a/haskell/src/SEL4/Kernel/VSpace/HaskellCPU.lhs +++ b/haskell/src/SEL4/Kernel/VSpace/HaskellCPU.lhs @@ -16,4 +16,4 @@ The generic Haskell-based CPU uses the capability space for virtual memory. > import SEL4.Kernel.VSpace.CSpace -% arch-tag: 0d0d5f20-d838-47f1-88b7-afdd7427dde8 + diff --git a/haskell/src/SEL4/Machine.lhs b/haskell/src/SEL4/Machine.lhs index b40cf01ec..cba732930 100644 --- a/haskell/src/SEL4/Machine.lhs +++ b/haskell/src/SEL4/Machine.lhs @@ -16,4 +16,4 @@ > import SEL4.Machine.RegisterSet > import SEL4.Machine.Hardware -% arch-tag: 57da9033-a344-40d4-9abb-2aeba95e840b + diff --git a/haskell/src/SEL4/Machine/Hardware.lhs b/haskell/src/SEL4/Machine/Hardware.lhs index 39dc4685c..02c98cd26 100644 --- a/haskell/src/SEL4/Machine/Hardware.lhs +++ b/haskell/src/SEL4/Machine/Hardware.lhs @@ -201,4 +201,4 @@ The constant "nullPointer" is a physical pointer guaranteed to be invalid. > nullPointer :: PPtr a > nullPointer = PPtr 0 -% arch-tag: 36b378a0-bd18-450e-8750-801303d45ef4 + diff --git a/haskell/src/SEL4/Machine/Hardware/ARM.lhs b/haskell/src/SEL4/Machine/Hardware/ARM.lhs index 48e7e0dc8..7e8dbc8c5 100644 --- a/haskell/src/SEL4/Machine/Hardware/ARM.lhs +++ b/haskell/src/SEL4/Machine/Hardware/ARM.lhs @@ -527,4 +527,4 @@ ARM page directories and page tables occupy four frames and one quarter of a fra > cacheLineBits = Platform.cacheLineBits > cacheLine = Platform.cacheLine -% arch-tag: 3e8808f8-c45e-4d7d-9111-4f3fccda1091 + diff --git a/haskell/src/SEL4/Machine/Hardware/ARM/QEmu.hs b/haskell/src/SEL4/Machine/Hardware/ARM/QEmu.hs index 769ca7a3b..1b8eea0be 100644 --- a/haskell/src/SEL4/Machine/Hardware/ARM/QEmu.hs +++ b/haskell/src/SEL4/Machine/Hardware/ARM/QEmu.hs @@ -212,4 +212,3 @@ foreign import ccall unsafe "qemu_arm_get_dfsr" foreign import ccall unsafe "qemu_arm_get_far" getFAR :: Ptr CallbackData -> IO VPtr --- arch-tag: 4371ACC8-49A8-4133-BCB5-EC346558446C diff --git a/haskell/src/SEL4/Machine/Hardware/Alpha.lhs b/haskell/src/SEL4/Machine/Hardware/Alpha.lhs index 38065bcf1..6677bbef8 100644 --- a/haskell/src/SEL4/Machine/Hardware/Alpha.lhs +++ b/haskell/src/SEL4/Machine/Hardware/Alpha.lhs @@ -109,4 +109,4 @@ > setRegister PC addr > setRegister NPC $ addr + 4 -% arch-tag: dc6aef28-0589-4de7-baef-d2ed4b4218f8 + diff --git a/haskell/src/SEL4/Machine/Hardware/HaskellCPU.lhs b/haskell/src/SEL4/Machine/Hardware/HaskellCPU.lhs index c4da3d09f..2abc0d363 100644 --- a/haskell/src/SEL4/Machine/Hardware/HaskellCPU.lhs +++ b/haskell/src/SEL4/Machine/Hardware/HaskellCPU.lhs @@ -67,4 +67,4 @@ > getFaultingPC = getRegister (Register HaskellCPU.PC) > setNextPC = setRegister (Register HaskellCPU.PC) -% arch-tag: 42bf0d02-88a4-45e2-8ec0-432beb5f20d1 + diff --git a/haskell/src/SEL4/Machine/RegisterSet.lhs b/haskell/src/SEL4/Machine/RegisterSet.lhs index 59c2374ee..a657daf0a 100644 --- a/haskell/src/SEL4/Machine/RegisterSet.lhs +++ b/haskell/src/SEL4/Machine/RegisterSet.lhs @@ -168,4 +168,4 @@ The "mask" function is a trivial function which, given a number of bits, returns > mask :: (Bits w, Num w) => Int -> w > mask bits = bit bits - 1 -% arch-tag: 2261b75e-5d0a-4b42-a807-ea4e33e42f9c + diff --git a/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs b/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs index 8c8009675..784a0e884 100644 --- a/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs +++ b/haskell/src/SEL4/Machine/RegisterSet/ARM.lhs @@ -43,4 +43,4 @@ This module defines the ARM register set. > sanitiseRegister CPSR v = (v .&. 0xf8000000) .|. 0x150 > sanitiseRegister _ v = v -% arch-tag: 7389f665-221a-4922-99f8-3769d9516056 + diff --git a/haskell/src/SEL4/Machine/RegisterSet/HaskellCPU.lhs b/haskell/src/SEL4/Machine/RegisterSet/HaskellCPU.lhs index b4cd50d01..52efd6b79 100644 --- a/haskell/src/SEL4/Machine/RegisterSet/HaskellCPU.lhs +++ b/haskell/src/SEL4/Machine/RegisterSet/HaskellCPU.lhs @@ -33,4 +33,4 @@ > frameRegisters = PC : SP : [AR0 .. AR7] > gpRegisters = [R0 .. R31] -% arch-tag: b9e526f6-506a-43ab-b50c-74c30b327c43 + diff --git a/haskell/src/SEL4/Model.lhs b/haskell/src/SEL4/Model.lhs index 2ab19dcf5..96f6bd5b4 100644 --- a/haskell/src/SEL4/Model.lhs +++ b/haskell/src/SEL4/Model.lhs @@ -22,4 +22,4 @@ > import SEL4.Model.Preemption > import SEL4.Model.Syscall -% arch-tag: 20826860-100b-4812-bd66-cb7d51e0d5d4 + diff --git a/haskell/src/SEL4/Model/Failures.lhs b/haskell/src/SEL4/Model/Failures.lhs index 853d178fa..0cece2f26 100644 --- a/haskell/src/SEL4/Model/Failures.lhs +++ b/haskell/src/SEL4/Model/Failures.lhs @@ -119,4 +119,4 @@ This trivial helper function is used to check that an argument is within an acce > unless (value >= fromIntegral minV && value <= fromIntegral maxV) $ > throw $ RangeError (fromIntegral minV) (fromIntegral maxV) -% arch-tag: 31C1388C-9B60-11D9-8215-000393DEF6D6 + diff --git a/haskell/src/SEL4/Model/PSpace.lhs b/haskell/src/SEL4/Model/PSpace.lhs index 3f63304ed..52d18b20f 100644 --- a/haskell/src/SEL4/Model/PSpace.lhs +++ b/haskell/src/SEL4/Model/PSpace.lhs @@ -313,4 +313,4 @@ The following predicate is used above to assert that the pointer is a valid poin > pointerInUserData :: PPtr Word -> KernelState -> Bool > pointerInUserData _ _ = True -% arch-tag: D34743A6-5491-11D9-A5ED-000393DEF6D6 + diff --git a/haskell/src/SEL4/Model/Preemption.lhs b/haskell/src/SEL4/Model/Preemption.lhs index d06eb1b2b..39ee679d8 100644 --- a/haskell/src/SEL4/Model/Preemption.lhs +++ b/haskell/src/SEL4/Model/Preemption.lhs @@ -59,4 +59,4 @@ In preemptible code, the kernel may explicitly mark a preemption point with the > Just irq -> throwError irq > Nothing -> return () -% arch-tag: 9355E52F-855B-47C6-B016-AE6B8C611A20 + diff --git a/haskell/src/SEL4/Model/StateData.lhs b/haskell/src/SEL4/Model/StateData.lhs index 26fa2145a..e98baa35a 100644 --- a/haskell/src/SEL4/Model/StateData.lhs +++ b/haskell/src/SEL4/Model/StateData.lhs @@ -263,4 +263,4 @@ The function "findM" searches a list, returning the first item for which the giv > r <- f x > if r then return $ Just x else findM f xs -% arch-tag: CBFB52AC-5491-11D9-AB6E-000393DEF6D6 + diff --git a/haskell/src/SEL4/Model/Syscall.lhs b/haskell/src/SEL4/Model/Syscall.lhs index ca4266372..fa7861936 100644 --- a/haskell/src/SEL4/Model/Syscall.lhs +++ b/haskell/src/SEL4/Model/Syscall.lhs @@ -39,4 +39,4 @@ The "syscall" function lifts code into the appropriate monads, and handles fault > Left e -> withoutPreemption $ hError e > Right b -> mFinalise b -% arch-tag: CEC74BF8-9541-4BEF-B9B0-9AB92BCC092F + diff --git a/haskell/src/SEL4/Object.lhs b/haskell/src/SEL4/Object.lhs index c3a44f45e..af5fbbd8e 100644 --- a/haskell/src/SEL4/Object.lhs +++ b/haskell/src/SEL4/Object.lhs @@ -33,4 +33,4 @@ > Capability(..), KernelObject(..), UserData(..), > isNullCap) -% arch-tag: 178b9a26-dd3f-489b-940b-205704164bc9 + diff --git a/haskell/src/SEL4/Object/AsyncEndpoint.lhs b/haskell/src/SEL4/Object/AsyncEndpoint.lhs index fc239e536..c187c4164 100644 --- a/haskell/src/SEL4/Object/AsyncEndpoint.lhs +++ b/haskell/src/SEL4/Object/AsyncEndpoint.lhs @@ -145,4 +145,4 @@ The following functions are specialisations of the "getObject" and "setObject" f > setAsyncEP :: PPtr AsyncEndpoint -> AsyncEndpoint -> Kernel () > setAsyncEP = setObject -% arch-tag: b0b6ba36-9713-415b-a96c-ad5b0f02c41d + diff --git a/haskell/src/SEL4/Object/CNode.lhs b/haskell/src/SEL4/Object/CNode.lhs index abffae631..a6c5e01e8 100644 --- a/haskell/src/SEL4/Object/CNode.lhs +++ b/haskell/src/SEL4/Object/CNode.lhs @@ -793,4 +793,4 @@ This helper function is used to load the capability transfer data from an IPC bu > ctReceiveIndex = CPtr w1, > ctReceiveDepth = fromIntegral w2 } -% arch-tag: AB52E196-5491-11D9-A15C-000393DEF6D6 + diff --git a/haskell/src/SEL4/Object/Endpoint.lhs b/haskell/src/SEL4/Object/Endpoint.lhs index d73f4971a..4342fba01 100644 --- a/haskell/src/SEL4/Object/Endpoint.lhs +++ b/haskell/src/SEL4/Object/Endpoint.lhs @@ -260,4 +260,4 @@ The following two functions are specialisations of "getObject" and > setEndpoint :: PPtr Endpoint -> Endpoint -> Kernel () > setEndpoint = setObject -% arch-tag: BD8F199C-5491-11D9-AE0C-000393DEF6D6 + diff --git a/haskell/src/SEL4/Object/Instances.lhs b/haskell/src/SEL4/Object/Instances.lhs index 699be26b7..ccee34c2d 100644 --- a/haskell/src/SEL4/Object/Instances.lhs +++ b/haskell/src/SEL4/Object/Instances.lhs @@ -155,4 +155,4 @@ By default, new threads are unable to change the security domains of other threa > KOUserData -> return UserData > _ -> typeError "UserData" o -% arch-tag: 23a13831-1203-43e3-8240-9f2d11f2ea9b + diff --git a/haskell/src/SEL4/Object/Interrupt.lhs b/haskell/src/SEL4/Object/Interrupt.lhs index 09394115b..c97654317 100644 --- a/haskell/src/SEL4/Object/Interrupt.lhs +++ b/haskell/src/SEL4/Object/Interrupt.lhs @@ -194,4 +194,4 @@ The following functions are used within this module to access the global interru > node <- liftM intStateIRQNode getInterruptState > locateSlot node (fromIntegral $ fromEnum irq) -% arch-tag: 7FC1EAA1-BAFF-460B-A97C-32EB5CB6CD3E + diff --git a/haskell/src/SEL4/Object/Interrupt/ARM.lhs b/haskell/src/SEL4/Object/Interrupt/ARM.lhs index 4c49aee0b..0fb0fbe98 100644 --- a/haskell/src/SEL4/Object/Interrupt/ARM.lhs +++ b/haskell/src/SEL4/Object/Interrupt/ARM.lhs @@ -29,4 +29,4 @@ This module defines the machine-specific interrupt handling routines for the ARM > invokeInterruptControl :: InterruptControl -> KernelP () > invokeInterruptControl _ = fail "invokeInterruptControl: not defined" -% arch-tag: 247C86BB-973A-41B4-AA68-9373A40DB338 + diff --git a/haskell/src/SEL4/Object/ObjectType.lhs b/haskell/src/SEL4/Object/ObjectType.lhs index 842f5fb9c..0a67b22e2 100644 --- a/haskell/src/SEL4/Object/ObjectType.lhs +++ b/haskell/src/SEL4/Object/ObjectType.lhs @@ -551,4 +551,4 @@ The following two functions returns the base and size of the object a capability > capUntypedSize (IRQHandlerCap {}) > = 1 -- error in haskell -% arch-tag: 64E4C155-9DEB-11D9-BC66-000393DEF6D6 + diff --git a/haskell/src/SEL4/Object/ObjectType/ARM.lhs b/haskell/src/SEL4/Object/ObjectType/ARM.lhs index 7db711bad..bba97af38 100644 --- a/haskell/src/SEL4/Object/ObjectType/ARM.lhs +++ b/haskell/src/SEL4/Object/ObjectType/ARM.lhs @@ -297,4 +297,4 @@ Create an architecture-specific object. > capUntypedSize (ASIDControlCap {}) = 1 `shiftL` (asidHighBits + 2) > capUntypedSize (ASIDPoolCap {}) = 1 `shiftL` (asidLowBits + 2) -% arch-tag: 0377d618-8fc7-4c7f-b4bb-df6da4be9bed + diff --git a/haskell/src/SEL4/Object/ObjectType/HaskellCPU.lhs b/haskell/src/SEL4/Object/ObjectType/HaskellCPU.lhs index f4c619fce..c6fc41880 100644 --- a/haskell/src/SEL4/Object/ObjectType/HaskellCPU.lhs +++ b/haskell/src/SEL4/Object/ObjectType/HaskellCPU.lhs @@ -27,4 +27,4 @@ This module contains operations on machine-specific object types for the Haskell > KernelF Fault (Maybe (Word, [Word])) > invokeObject = undefined -% arch-tag: 41639328-da7f-40c1-a873-0eb90e0a682a + diff --git a/haskell/src/SEL4/Object/Structures.lhs b/haskell/src/SEL4/Object/Structures.lhs index 1be4e2dcc..f57065900 100644 --- a/haskell/src/SEL4/Object/Structures.lhs +++ b/haskell/src/SEL4/Object/Structures.lhs @@ -429,4 +429,4 @@ This type is used to represent a frame in the user's address space. > maxFreeIndex :: Int -> Int > maxFreeIndex sizeBits = bit sizeBits -% arch-tag: f7061313-650e-4ae7-addc-0d730b86722f + diff --git a/haskell/src/SEL4/Object/Structures/ARM.lhs b/haskell/src/SEL4/Object/Structures/ARM.lhs index b5bcbaa36..852f2722e 100644 --- a/haskell/src/SEL4/Object/Structures/ARM.lhs +++ b/haskell/src/SEL4/Object/Structures/ARM.lhs @@ -97,4 +97,4 @@ ASIDs are mapped to address space roots by a global two-level table. The actual > asidHighBitsOf :: ASID -> ASID > asidHighBitsOf asid = (asid `shiftR` asidLowBits) .&. mask asidHighBits -% arch-tag: 814D2696-C9C8-4A95-A7AC-BBFC197BAB71 + diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs index 678e8f525..41eedc581 100644 --- a/haskell/src/SEL4/Object/TCB.lhs +++ b/haskell/src/SEL4/Object/TCB.lhs @@ -654,4 +654,4 @@ identified by "tcbPtr". > threadSet (\tcb -> tcb { tcbContext = uc' }) tptr > return a -% arch-tag: 71d10ec9-496e-45bf-9718-b12726324443 + From 6f5a3670109d14f5a8b8899faaaafed023f75709 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 19 Jul 2014 15:02:32 +0200 Subject: [PATCH 07/13] add .gitignore --- .gitignore | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 000000000..45b2eaf47 --- /dev/null +++ b/.gitignore @@ -0,0 +1,39 @@ +# +# Copyright 2014, General Dynamics C4 Systems +# +# This software may be distributed and modified according to the terms of +# the GNU General Public License version 2. Note that NO WARRANTY is provided. +# See "LICENSE_GPLv2.txt" for details. +# +# @TAG(GD_GPL) +# + +# generated python bytecode +**.pyc + +# latex generated files +**.aux +**.log +**.out +**.lof +**.lot +**.bbl +**.blg +**.toc +**.mpx + +manual/env.tex +manual/manual.pdf + +haskell/doc/refman.pdf +haskell/doc/version.txt + +haskell/doc/figures/clientkernel.pdf +haskell/doc/figures/clientserver.pdf +haskell/doc/figures/derive.pdf +haskell/doc/figures/ipctransfer.pdf +haskell/doc/figures/truncation.pdf + +# haskell generated files +**.lhs-boot +haskell/dist From 3ffeaac26d147ea0e186b56249321804ac3f7929 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 19 Jul 2014 10:54:29 +0200 Subject: [PATCH 08/13] Retire old dft package; resurrect Haskell manual. Text is still out of date, but the document builds. Added out-of-date warning text. --- haskell/INSTALL | 3 - haskell/doc/Makefile | 30 ++--- haskell/doc/README | 7 +- haskell/doc/disy.sty | 178 +++++++++++++++++++++++++ haskell/doc/figures/truncation.mp | 7 + haskell/doc/haskell.tex | 15 ++- haskell/doc/lambdaTeX.sty | 3 - haskell/doc/overview.tex | 46 ++++--- haskell/doc/pubs.bib | 12 +- haskell/doc/refman.tex | 171 +++++++++++++++--------- haskell/src/SEL4/Object/CNode.lhs | 8 +- haskell/src/SEL4/Object/Interrupt.lhs | 12 +- haskell/src/SEL4/Object/ObjectType.lhs | 8 +- haskell/src/SEL4/Object/Structures.lhs | 2 +- haskell/src/SEL4/Object/TCB.lhs | 24 ++-- haskell/src/SEL4/Object/Untyped.lhs | 4 +- 16 files changed, 378 insertions(+), 152 deletions(-) create mode 100644 haskell/doc/disy.sty diff --git a/haskell/INSTALL b/haskell/INSTALL index 1fa5bccaf..114f84f2c 100644 --- a/haskell/INSTALL +++ b/haskell/INSTALL @@ -26,9 +26,6 @@ To build it: arm-isabuilder - build the library: runhaskell Setup.hs build - There will be a few warnings about unused definitions in the -boot files; - if building with -fvia-C (the default for GHC 6.6) there will also be many - warnings about implicitly defined functions. These are ok. - install: runhaskell Setup.hs install --user diff --git a/haskell/doc/Makefile b/haskell/doc/Makefile index ae5add102..de6fb9c82 100644 --- a/haskell/doc/Makefile +++ b/haskell/doc/Makefile @@ -8,15 +8,7 @@ # @TAG(GD_GPL) # -dftPath ?= ./dft/ - -dftExtraTeXInputs= - -Target = refman.pdf - -all: ${Target} - -include ${dftPath}/rules/main.mk +all: refman.pdf LHSFILES=$(wildcard ../src/SEL4/*.lhs) \ $(wildcard ../src/SEL4/Machine/*.lhs) \ @@ -31,24 +23,28 @@ TEXFILES=$(wildcard *.tex) FIGURE_SOURCES=$(wildcard figures/*.mp) FIGURES=$(patsubst %.mp,%.pdf,$(FIGURE_SOURCES)) -SOURCES=$(LHSFILES) $(TEXFILES) $(FIGURES) version.aux functions.aux +SOURCES=$(LHSFILES) $(TEXFILES) $(FIGURES) version.txt functions.aux -%.mps: %.mp - echo $< $@ - mpost $< && mv -f $(notdir $(@:.mps=.1)) $@ +figures/%.mps: figures/%.mp + @echo $< $@ + @(cd figures; mpost --tex=latex $* && mv -f $*.1 $*.mps) figures/%.pdf: figures/%.mps - (cd figures && mptopdf $*.mps && mv $*-mps.pdf $*.pdf) + @(cd figures && mptopdf $*.mps && mv $*-mps.pdf $*.pdf) -version.aux: always - echo "\softwareversion{`hg parent --template '{date|shortdate} (Revision {node|short})\n'`}" > $@ +version.txt: always + @echo "`git log -n 1 --date=short --abbrev=20 --abbrev-commit --format='%h %ad' HEAD`" > $@ .PHONY: always functions.aux: $(LHSFILES) perl mkfunctions.pl -${Target}: ${SOURCES} +refman.pdf: ${SOURCES} + pdflatex refman + bibtex refman + pdflatex refman + pdflatex refman clean: rm -f *.aux *.toc *.bbl *.blg *.dvi *.log *.out \ diff --git a/haskell/doc/README b/haskell/doc/README index 80f6feb07..6dc03eb3e 100644 --- a/haskell/doc/README +++ b/haskell/doc/README @@ -8,9 +8,4 @@ # @TAG(GD_GPL) # -To build the documentation: - -1. make - Alternatively, if you have xelatex, and the necessary fonts - (Times, Helvetica, Courier, and Fontin Sans) are installed: - make xelatex=yes +To build the documentation, run `make` diff --git a/haskell/doc/disy.sty b/haskell/doc/disy.sty new file mode 100644 index 000000000..b8e95debc --- /dev/null +++ b/haskell/doc/disy.sty @@ -0,0 +1,178 @@ +% +% Copyright 2014, NICTA +% +% This software may be distributed and modified according to the terms of +% the BSD 2-Clause license. Note that NO WARRANTY is provided. +% See "LICENSE_BSD2.txt" for details. +% +% @TAG(NICTA_BSD) +% + +% disy.sty +% +% Document style for reports by the UNSW Distributed Systems and +% Operating Systems (DiSy) group. +% +% Uses Andrew O'Brien's fancy title page... +% +% Written 2000-08-12 by Gernot Heiser +% +% $Id: disy.sty,v 1.2 2009-02-04 03:13:15 ikuz Exp $ + +% OPTIONS: +% color: use colour logos +% cmyk: will generate cmyk colours rather than rgb colours +% this may prove more reliable on some printers +% but is inclined to look odd on monitors +% nicta: use NICTA logo besides UNSW +% nictaonly: use NICTA logo but no UNSW +% +% COMMANDS: +% \AuthorEmail Author's email address (default: disy@cse) + +\ProvidesPackage{disy} +\RequirePackage{graphicx} +\RequirePackage{url} +\RequirePackage{color} + +\DeclareOption{color}{\Colortrue} +\DeclareOption{colour}{\Colortrue} +\DeclareOption{cmyk}{\CMYKtrue} +\DeclareOption{nicta}{\NICTAtrue} +\DeclareOption{nictaonly}{\NICTAtrue\UNSWfalse} + +\newif\ifColor \Colorfalse +\newif\ifNICTA \NICTAfalse +\newif\ifCMYK \CMYKfalse +\newif\ifUNSW \UNSWtrue % for historic reasons + +\ProcessOptions + +\ifColor + \ifCMYK + \definecolor{nictablue}{cmyk}{1.0,0.18,0.0,0.51} + \definecolor{nictagreen}{cmyk}{1.0,0.0,0.69,0.43} + \else + \definecolor{nictablue}{rgb}{.000,.348,.508} + \definecolor{nictagreen}{rgb}{.020,.426,.328} + \fi +\else + \definecolor{nictablue}{cmyk}{0,0,0,1} % black + \definecolor{nictagreen}{cmyk}{0,0,0,1} % black +\fi +\newif\ifHave@HyperRef\Have@HyperReffalse + +\AtBeginDocument{\@ifpackageloaded{hyperref}{\Have@HyperReftrue}{}} + +\newcommand{\AuthorEmail}[1]{\def\AuthorEmailString{#1}} + +\newcommand{\CrestFileName}{\ifColor unicrest-colour\else unicrest-screen\fi} +%\newcommand{\LogoFileName}{\ifColor nicta-col\else nicta-bw\fi} +\AuthorEmail{disy@cse.unsw.edu.au} + +\newlength{\centeroffset} +\setlength{\centeroffset}{-0.5\oddsidemargin} +\addtolength{\centeroffset}{0.5\evensidemargin} + +\def\maketitle{ + % to suppress overfull bars in ``draft'' mode: + \newlength{\saveOverfullRule} + \setlength{\saveOverfullRule}{\overfullrule} + \setlength\overfullrule{0pt} + + \thispagestyle{empty} + \vspace*{\stretch{1}} + \noindent\hspace*{\centeroffset} + + \begin{minipage}{\textwidth}\flushright% + \urlstyle{sf}% + \raisebox{34mm}[0pt][0pt]{% + \newcommand{\LogoW}{21mm}% + \newlength{\ERTOSw}% + %\setlength{\ERTOSw}{\textwidth}% + %\addtolength{\ERTOSw}{-\LogoW}\addtolength{\ERTOSw}{-2em}% + \settowidth{\ERTOSw}{{\sf\large http://ssrg.nicta.com.au/}}% + %\settowidth{\ERTOSw}{{\sf\large Operating Systems Group}}% + %\newcommand{\NICTAlogo}{\includegraphics[width=\LogoW]{imgs/\LogoFileName}}% + \noindent\sf% + \begin{minipage}[b]{\textwidth}\sf\large% + \hspace*{-10mm}% + \ifNICTA% + \color{nictablue}% + \begin{minipage}[b]{1.1\ERTOSw}\urlstyle{sf}% + Trustworthy Systems\\ + \url{http://ssrg.nicta.com.au/}\\~ + \end{minipage} + \hfill +% \ifx\undefined\hyperref% +% \NICTAlogo% +% \else% +% \raisebox{2mm}{\href{http://nicta.com.au}{\NICTAlogo}}% +% \fi% +% \else~ + \fi% + \end{minipage}% + \hspace*{-4mm}% + }% + % + \flushright + {\Huge\bfseries + \@title\\} + \vspace*{\stretch{2}} + \noindent\rule[-1ex]{\textwidth}{5pt}\\[2.5ex] + {\Large \bfseries \@author}\\ + \ifUNSW + \vspace{2ex} + \else + \urlstyle{sf} + \ifHave@HyperRef + \url{\AuthorEmailString}\\[2ex] + \else + \AuthorEmailString\\[2ex] + \fi + \fi + {\sf \hfill{\Large \@date}}\\[2ex] + \end{minipage} + + \vspace{\stretch{1}} + \noindent\hspace*{\centeroffset}\begin{minipage}{\textwidth} + \flushright + + \end{minipage} + \vspace{\stretch{2}} + + \vfill + + \begin{minipage}{\textwidth} + \flushright + {\noindent\sf% + \ifUNSW + \newcommand{\DiSyCrest} + {\includegraphics[height=25mm,clip]{imgs/\CrestFileName}}% + \newlength{\DiSyCrestwdth}\settowidth{~\DiSyCrestwdth}{\DiSyCrest}% + \newlength{\DiSyFtwdth}% + \setlength{\DiSyFtwdth}{\textwidth}% + \addtolength{\DiSyFtwdth}{-\DiSyCrestwdth}% + \addtolength{\DiSyFtwdth}{-1em}% + \begin{minipage}[b]{0.7\textwidth}\flushright + \urlstyle{sf} + \ifHave@HyperRef + \url{\AuthorEmailString}\\ + \else + \AuthorEmailString\\ + \fi + \url{http://www.cse.unsw.edu.au/~disy/}\\ + Operating Systems and Distributed Systems Group\\ + School of Computer Science and Engineering\\ + The University of New South Wales\\ + UNSW Sydney 2052, Australia%\vspace*{0.6ex}% + \end{minipage}% + \hspace{1em}\DiSyCrest% + \fi + } + \end{minipage} + + \clearpage + % reset overfull rule + \setlength{\overfullrule}{\saveOverfullRule} +}%\maketitle diff --git a/haskell/doc/figures/truncation.mp b/haskell/doc/figures/truncation.mp index c9a41c88a..22427266e 100644 --- a/haskell/doc/figures/truncation.mp +++ b/haskell/doc/figures/truncation.mp @@ -1,3 +1,10 @@ +verbatimtex +\documentclass[12pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{mathptmx} +\begin{document} +etex; + input boxes; beginfig(1); diff --git a/haskell/doc/haskell.tex b/haskell/doc/haskell.tex index 0939181a0..c96f7acc1 100644 --- a/haskell/doc/haskell.tex +++ b/haskell/doc/haskell.tex @@ -10,7 +10,7 @@ This chapter describes the construction of the Haskell model presented in the following chapters. It is not necessary to read this chapter to understand the seL4 API, but it will be helpful for those who wish to read the Haskell code. -\section[intro]{Introduction to Haskell} +\section{Introduction to Haskell}\label{sec:haskell.intro} Haskell is a general purpose functional programming language~\cite{peytonjones03haskell}. It is in widespread use in the research and education communities; several universities use it in introductory programming courses. @@ -23,7 +23,7 @@ The features of Haskell that are most relevant to this project are: A more detailed introduction to Haskell is outside the scope of this document. Please refer to the online Haskell tutorials~\cite{haskell-tutorial,monad-tutorial} for more information. -\section[modules]{Modules} +\section{Modules}\label{sec:haskell.modules} The Haskell model is split into a hierarchy of modules. At the top level is "module SEL4", which contains no real code, but exports the entire external interface of the kernel model. Below this are five modules that serve to separate the high-level and low-level parts of the model; each of these corresponds to one of the following five chapters in this report. @@ -38,7 +38,7 @@ The five modules have the following purposes: Each of these modules is further divided into smaller modules implementing separate functional areas. For example, "module SEL4.Kernel" contains a module implementing capability space lookups, "module SEL4.Kernel.CSpace". -\section[state-monads]{System State and Monads} +\section{System State and Monads}\label{sec:haskell.state-monads} \subsection{The State Monad} @@ -86,7 +86,8 @@ Again, Haskell's strict typing requires all transitions in and out of the "Error The Haskell kernel model makes use of the "ErrorT" transformer to abort operations that are preempted or cannot complete successfully. The first type parameter of "ErrorT" is a type that represents the error; there are several such types defined in seL4, in \autoref{sec:model.failures} and \autoref{sec:model.preemption}. -\subsection[system-state]{System State} +\subsection{System State} +\label{sec:haskell.state-monads.system-state} The state of the simulated kernel is stored in values of type "KernelState". Most functions in the model are in the monad "KernelMonad", and are therefore state transformation functions that operate on a value of type "KernelState". @@ -96,13 +97,13 @@ The other values present in the "KernelState" structure are global kernel data, The "KernelState" value is added to "KernelMonad" by a monad transformer, "StateT". This adds the state to an existing monad, the \emph{machine monad}, the type of which depends on the machine being simulated. See \autoref{sec:haskell.simulator.monad}. -\subsection[pspace]{Physical Memory Model} +\subsection{Physical Memory Model}\label{sec:haskell.state-monads.pspace} The simulated kernel's physical memory is modelled by the Haskell type "PSpace", defined in \autoref{sec:model.pspace}. The contents of each address in this space are typed; that is, the model keeps a record of whether they are allocated, and whether they contain either integer data, or a specific type of kernel object. Accesses to objects of the wrong type, or with an incorrectly aligned address, are detected by the model and disallowed. For simulator performance reasons, and to make the operation of the virtual memory related parts of the model more realistic, the "PSpace" contains only typed kernel objects; it does not contain data accessible to user level. Instead, regions occupied by such data are represented by a "UserData" object, which has no contents. The actual data is stored separately, and is accessed via the machine monad. -\section[simulator]{The Simulator} +\section{The Simulator}\label{sec:haskell.simulator} The kernel model functions as one half of a complete system model. The other half is the CPU simulator, responsible for modelling the execution of user-level programs and the operation of hardware devices. @@ -116,7 +117,7 @@ The set of events supported by the Haskell model is defined by the type "Event", Several aspects of the kernel's API and behaviour vary depending on the architecture of the host machine. The model contains abstract interfaces to the components that change; the interfaces are implemented in separate modules, selected using the preprocessor. -\subsection[monad]{Simulator Interface} +\subsection{Simulator Interface}\label{sec:haskell.simulator.monad} The state of the simulated machine is accessed via a monad, the type of which depends on which CPU simulator is in use --- again, selected using the preprocessor. For example, for a simulator implemented entirely in Haskell, this monad is likely to be "State", with a data structure containing the machine's state data. If the simulator is implemented externally, and communicates with the kernel via the Haskell foreign function interface, then the machine monad will be "IO" (or some transformation of "IO"), allowing functions in it to call out to the external simulator. diff --git a/haskell/doc/lambdaTeX.sty b/haskell/doc/lambdaTeX.sty index 1560c142b..1228f7386 100644 --- a/haskell/doc/lambdaTeX.sty +++ b/haskell/doc/lambdaTeX.sty @@ -64,7 +64,6 @@ % immediately following the -- should be a space, anyway. \ProvidesPackage{lambdaTeX} -\BeginPackage \catcode`@=11 @@ -1493,8 +1492,6 @@ \catcode`@=12 -\EndPackage - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% THE END %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/haskell/doc/overview.tex b/haskell/doc/overview.tex index 4adf76328..67745733a 100644 --- a/haskell/doc/overview.tex +++ b/haskell/doc/overview.tex @@ -8,7 +8,7 @@ % @TAG(GD_GPL) % -\section[intro]{Introduction} +\section{Introduction}\label{sec:overview.intro} This chapter provides an overview of the \emph{seL4} kernel. It concentrates on the conceptual differences between seL4 and existing @@ -21,7 +21,7 @@ to authorise system calls and making kernel data structures first class objects whose allocation is performed by user-level operating system personalities. -\section[caps]{Capabilities, Endpoints, and System Calls} +\section{Capabilities, Endpoints, and System Calls}\label{sec:overview.caps} Each user-space thread in the system possesses a set of \emph{capabilities}. A capability provides the thread that possesses it with the ability to perform one @@ -52,7 +52,7 @@ depend on the type of the kernel object that the capability refers to. For most object types, the kernel itself is the recipient of the message; however, messages may also be sent to other user-level threads. -\subsection[ipc]{Synchronous Endpoints and IPC} +\subsection{Synchronous Endpoints and IPC}\label{sec:overview.caps.ipc} The basic inter-process communication (or \emph{IPC}) operation is coordinated using \emph{endpoint} objects. An endpoint is a small kernel object which @@ -75,9 +75,10 @@ typically will be first in, first out order. \begin{figure} \centering \includegraphics{figures/ipctransfer} -\caption[ipctransfer]{IPC operation, without message buffers. The solid lines represent +\caption{IPC operation, without message buffers. The solid lines represent references to kernel objects; the dashed lines represent the transfer of control and data between the threads.} +\label{fig:ipctransfer} \end{figure} Since it is only possible to wait for messages from one specific endpoint at a @@ -96,14 +97,15 @@ immutable and opaque: a badged capability cannot be used with the Mint operation When a message is sent using a badged endpoint capability, the badge is passed to the recipient along with the rest of the message. See -\autoref{fig:.ipctransfer} for an example. +\autoref{fig:ipctransfer} for an example. \subsubsection{Message Transfers} \begin{figure} \centering \includegraphics{figures/truncation} -\caption[truncation]{Truncation of a message when one of the IPC buffer capabilities is +\caption{Truncation of a message when one of the IPC buffer capabilities is missing.} +\label{fig:truncation} \end{figure} Message transfers work by transferring the contents of a certain number of @@ -121,7 +123,7 @@ first word that reflects the actual transfer performed. If the message buffer must be used to transfer the requested number of message words, and either the sender's or the recipient's message buffer capability is missing, the message -will be truncated as shown in \autoref{fig:.truncation}. Note that the +will be truncated as shown in \autoref{fig:truncation}. Note that the sender cannot tell that this has happened, as informing it would open a covert channel from the recipient to the sender. The recipient is not explicitly notified either, though the message length specified in the first word will be @@ -180,7 +182,7 @@ Servers generally run a loop which waits for a message, handles the received mes \subsection{System Calls} -\Autoref{fig:.clientkernel} shows a request being made of the kernel by a +\autoref{fig:clientkernel} shows a request being made of the kernel by a client thread. The client possesses a capability to a kernel object, and a designated \emph{reply capability}, which is an endpoint capability that the client (or a system thread controlling the client) has nominated to be used @@ -190,9 +192,10 @@ invoked kernel object. \begin{figure} \centering \includegraphics{figures/clientkernel} -\caption[clientkernel]{A request by a client for a kernel service. The dotted lines +\caption{A request by a client for a kernel service. The dotted lines represent the conceptual flow of control and data during the request.} +\label{fig:clientkernel} \end{figure} After receiving a message from a client thread, the kernel determines which @@ -201,10 +204,11 @@ contents of the message; it then performs the operation if possible. If the user \begin{figure} \centering \includegraphics{figures/clientserver} -\caption[clientserver]{A request by a client for a service provided by a user-level server.} +\caption{A request by a client for a service provided by a user-level server.} +\label{fig:clientserver} \end{figure} -\Autoref{fig:.clientserver} shows the procedure followed when a client +\autoref{fig:clientserver} shows the procedure followed when a client requests a service provided by a user-level server thread. Rather than invoke a kernel object capability, the client invokes an endpoint which represents the service; the server thread receives the message, determines the identity @@ -296,7 +300,7 @@ powers of two), though the minimum and maximum sizes are specific to each implementation and type. Other objects are of fixed, implementation-specific size. -\section[threads]{Threads} +\section{Threads}\label{sec:overview.threads} Unlike previous versions of L4, threads in seL4 have no global identifier visible outside the kernel. A thread is identified only by the CSpace address @@ -342,7 +346,7 @@ again until a Resume operation is performed on it. An CopyRegisters or ReadRegisters operation may optionally include a Suspend operation on the source thread. \end{description} -\section[cspace]{Capability Address Spaces} +\section{Capability Address Spaces}\label{sec:overview.cspace} The capability space is represented by a \emph{guarded capability table}, which is similar to a guarded page table~\cite{Liedtke-94a}. The nodes of the @@ -356,8 +360,6 @@ opaque to user-space code. The format of entries is the same at all levels of the table. There is also a slot in each TCB, which is used to store a capability to the root CNode. -% XXX describe entry format? - The capability table is constructed by copying a capability to the root CNode into the TCB's root slot, capabilities to lower-level CNodes into the root CNode's slots, and so on. The number of address bits resolved by each CNode @@ -368,7 +370,7 @@ translating address bits starting at the page table root capability. Note that all CNodes are required to resolve at least one address bit, to prevent infinite loops in the capability lookup code. -\subsection[mdb]{The Mapping Database} +\subsection{The Mapping Database}\label{sec:overview.cspace.mdb} The kernel keeps a record of the \emph{derivation tree} for capabilities. This tree is stored in the \emph{mapping database}, and is used when revoking a @@ -392,7 +394,7 @@ access to untyped memory. This document describes the API for kernels that have a mapping database. -\subsection[cnodes]{CNode Operations} +\subsection{CNode Operations}\label{sec:overview.cspace.cnodes} User-level tasks possessing a capability to a CNode may perform any of five operations on the capabilities stored in the tree of which that CNode is the @@ -447,7 +449,7 @@ fail with a "DeleteFirst" error. As the error name suggests, the caller should call Delete on destination slots first, if there is any possibility that they might contain valid capabilities. This restriction also applies to the destination slot for Rotate, unless it is the same as the second source slot. -\subsection[rights]{Capability Rights} +\subsection{Capability Rights}\label{sec:overview.cspace.rights} The set of operations which may be performed on a given capability are determined by the type of the object that the capability refers to, and a set @@ -467,7 +469,7 @@ Newly created capabilities have all rights. They may be reduced when performing Copy, Mint or Move operations, either via a CSpace invocation or a capability transfer IPC. -\section[faults]{Faults and Exceptions} +\section{Faults and Exceptions}\label{sec:overview.faults} Whenever a user-level task raises a fault, the kernel will suspend it and send a \emph{fault call} to the thread's \emph{fault handler @@ -480,7 +482,7 @@ fault if possible. The recipient may take any appropriate action to handle the f Events that generate fault calls include missing capabilities, missing virtual memory mappings, non-seL4 system calls, and architecture-defined exceptions such as illegal instructions. The content of the fault calls, and the semantics of the replies, depends on the type of fault. Definitions for specific types of fault can be found in \autoref{sec:api.faults} -\section[vm]{Virtual Address Spaces} +\section{Virtual Address Spaces}\label{sec:overview.vm} Many modern hardware architectures dictate specific page table formats to be used by the kernel to implement virtual memory. These usually require the @@ -516,7 +518,7 @@ CNode objects. As the source parameters of such operations are always capabilities (in the CSpace), it is not possible to copy mappings between different locations in VSpace without possessing an appropriate capability. -\section[async-ipc]{Asynchronous IPC} +\section{Asynchronous IPC}\label{sec:overview.async-ipc} In some situations, it is appropriate to provide an asynchronous notification of an event. The kernel provides an \emph{asynchronous IPC} operation for this @@ -547,7 +549,7 @@ are waiting on the same endpoint when a message is sent to it, the kernel chooses one of them to deliver the message. The algorithm for choosing a thread is not specified, but typically will be first in, first out order. -\section[interrupts]{Interrupts} +\section{Interrupts}\label{sec:overview.interrupts} Interrupt handling in seL4 is performed using two special types of kernel capability. These capabilities cannot be created using the Retype operation, diff --git a/haskell/doc/pubs.bib b/haskell/doc/pubs.bib index 2ffe12233..aa71f7abe 100644 --- a/haskell/doc/pubs.bib +++ b/haskell/doc/pubs.bib @@ -1,3 +1,7 @@ +@string{proc = "Proceedings of the "} +@string{hotos = "Workshop on Hot Topics in Operating Systems"} +@string{hotos05 = proc#"10th "#hotos} + @inproceedings{wadler92essence, author = {Philip Wadler}, title = {The essence of functional programming}, @@ -33,11 +37,9 @@ author = {Harvey Tuch and Gerwin Klein and Gernot Heiser}, title = {{OS} Verification --- Now!}, booktitle = hotos05, - pages = xyz, + pages = {7--12}, year = 2005, address = {Santa Fe, NM, USA}, - format = "pdf", - keywords = {nicta, L4, l4verified}, month = jun } @@ -45,11 +47,7 @@ author = "Jochen Liedtke", title = "Page Table Structures For Fine-Grain Virtual Memory", journal = "IEEE Technical Committee on Computer Architecture Newsletter", - month = xyz, year = 1994, - pages = xyz, - keywords = "GPT", - heldby = "gernot" } @Misc{Pistachio:URL, diff --git a/haskell/doc/refman.tex b/haskell/doc/refman.tex index 725a31556..1b951d72b 100644 --- a/haskell/doc/refman.tex +++ b/haskell/doc/refman.tex @@ -8,18 +8,33 @@ % @TAG(GD_GPL) % -\documentclass{ertos-book} - -\title{seL4 Reference Manual} -\author{Philip Derrin, Dhammika Elkaduwe, Kevin Elphinstone} -\documentnumber=10200 -% \documentrevision=0 -\copyrightyear=2006 -\licence{restricted} -\input{version.aux} +\documentclass[a4paper,11pt,twoside]{report} +\usepackage[colour,nictaonly]{disy} \usepackage{comment} \usepackage{ifxetex,ifpdf} +\usepackage{alltt} +\usepackage[T1]{fontenc} + +\usepackage[margin=33mm]{geometry} +\usepackage{cite,fancyhdr,microtype,tocloft} + +\pagestyle{fancyplain} +\lhead[\fancyplain{}{\sl\thepage}]{\fancyplain{}{\sl\rightmark}} +\chead{} +\rhead[\fancyplain{}{\sl\leftmark}]{\fancyplain{}{\sl\thepage}} +\lfoot[\fancyplain{\sl\thepage}{}]{} +\cfoot{} +\rfoot[]{\fancyplain{\sl\thepage}{}} + +\definecolor{linkcolor}{rgb}{0,0,0.4} +\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor, + filecolor=linkcolor,urlcolor=linkcolor]{hyperref} + +\setlength{\cftsubsecnumwidth}{4em} +\setlength{\cftsecnumwidth}{6ex} + +\newcommand{\softwareversion}{\input{version.txt}} % Definitions of the appearance of the typeset Haskell code \ifxetex @@ -39,7 +54,6 @@ %\newenvironment{impdetails}{ % \ifimpdetails\begin{comment}\fi}{\ifimpdetails\end{comment}\fi} -\usepackage{cite} \usepackage{lambdaTeX} % Workaround for conflict between PDFTeX and lambdaTeX @@ -62,18 +76,31 @@ \typeout{If TeX stops here, run mkfunctions.pl to generate functions.aux} \input{functions.aux} -\bibliographystyle{plain} - \hyphenation{C-Space C-Spaces C-Node C-Nodes Has-kell Send-Wait Ex-change-Reg-ist-ers Thread-Con-trol} \begin{document} -% Re-enable lambdaTeX's active < and > -\catcode`\<=\active -\catcode`\>=\active +\title{seL4 Haskell Manual} +\author{Trustworthy~Systems~Team, NICTA} +\AuthorEmail{ssrg@nicta.com.au} +\date{\softwareversion} -\chapter*{Acknowledgements} +\maketitle + \urlstyle{sf} + \thispagestyle{empty} + + \vfill + + \copyright\ General Dynamics C4 Systems.\\ + + \textsc{All rights reserved}. + + % Acknowledgements + \thispagestyle{empty} + \vfill + \renewcommand{\abstractname}{Acknowledgements} + \begin{abstract} The seL4 project team would like to acknowledge the following people and teams (in no particular order) who have contributed to seL4 in some way. Apologies if we missed you. @@ -89,18 +116,37 @@ Jonathon Shapiro has also provided insightful interaction on many occasions, and his work on EROS and its successor Coyotos has also influenced seL4's design. -We would also like to thank Gerwin Klein and his \emph{l4.verified} - project team at NICTA for their insights and continual feedback on - our work. David Cock deserves special mention for his work on - bringing the ARM simulator into being. +We would also like to thank Gerwin Klein and his L4.verified +project team at NICTA for their insights and continual feedback on +our work. David Cock deserves special mention for his work on +bringing the ARM simulator into being. -Finally, we would like to thank members of the ERTOS program here at -NICTA for their daily interaction and input. +\vspace{5ex} +\begin{center} +{\large\textbf{Warning}} +\end{center} +This manual is currently out of date. While the Haskell code itself is kept +up-to-date, the text in this manual describes an old version of seL4 and uses +outdated/deprecated terminology. +\begin{center} +Use with caution. +\end{center} +\end{abstract} + + \thispagestyle{empty} + + \cleardoublepage + \setcounter{page}{1} + \tableofcontents + + \cleardoublepage + \setcounter{page}{1} + \pagenumbering{arabic} + +% Re-enable lambdaTeX's active < and > +\catcode`\<=\active +\catcode`\>=\active -National ICT Australia is funded by the Australian Government's -Department of Communications, Information Technology, and the Arts and -the Australian Research Council through \emph{Backing Australia's -Ability} and the ICT Research Centre of Excellence programs. \part{Introduction} @@ -115,115 +161,115 @@ from user level. This source code is executable --- not pseudocode --- and forms part of a simulator which can be used to examine the behaviour of a running seL4 kernel. -\Autoref{sec:overview} provides an overview of the seL4 API. \Autoref{sec:haskell} briefly discusses Haskell, and the manner in which we have applied it to construct the reference implementation. The remaining chapters are generated directly from the Haskell source code of the reference implementation, and contain all of the code (apart from some Haskell-specific implementation details, such as compiler and pre-processor directives). +\autoref{sec:overview} provides an overview of the seL4 API. \autoref{sec:haskell} briefly discusses Haskell, and the manner in which we have applied it to construct the reference implementation. The remaining chapters are generated directly from the Haskell source code of the reference implementation, and contain all of the code (apart from some Haskell-specific implementation details, such as compiler and pre-processor directives). -\chapter[overview]{seL4 Overview} +\chapter{seL4 Overview}\label{sec:overview} \input{overview.tex} -\chapter[haskell]{Haskell Model Overview} +\chapter{Haskell Model Overview}\label{sec:haskell} \input{haskell.tex} \part{Annotated Source Code} -\chapter[api]{Kernel API} +\chapter{Kernel API}\label{sec:api} This chapter documents the parts of the kernel that interact directly with user-level code. -\section[types]{Kernel Object Types} +\section{Kernel Object Types}\label{sec:api.types} \input{../src/SEL4/API/Types.lhs} -\section[types.universal]{Machine-Independent Object Types} +\section{Machine-Independent Object Types}\label{sec:api.types.universal} \input{../src/SEL4/API/Types/Universal.lhs} -\section[invocation]{Kernel Object Invocations} +\section{Kernel Object Invocations}\label{sec:api.invocation} \input{../src/SEL4/API/Invocation.lhs} -\section[syscall]{System Calls} +\section{System Calls}\label{sec:api.syscall} \input{../src/SEL4/API/Syscall.lhs} -\section[failures]{System Call Failures} +\section{System Call Failures}\label{sec:api.failures} \input{../src/SEL4/API/Failures.lhs} -\section[faults]{Faults and Exceptions} +\section{Faults and Exceptions}\label{sec:api.faults} \input{../src/SEL4/API/Faults.lhs} -\chapter[kernel]{Kernel Operations} +\chapter{Kernel Operations}\label{sec:kernel} This chapter documents operations within the kernel that are not directly related to a single kernel object. -\section[cspace]{Capability Space Lookups} +\section{Capability Space Lookups}\label{sec:kernel.cspace} \input{../src/SEL4/Kernel/CSpace.lhs} -\section[thread]{Threads and Scheduling} +\section{Threads and Scheduling}\label{sec:kernel.thread} \input{../src/SEL4/Kernel/Thread.lhs} -\section[init]{Bootstrapping the Kernel} +\section{Bootstrapping the Kernel}\label{sec:kernel.init} \input{../src/SEL4/Kernel/Init.lhs} -\section[faulthandler]{Handling Faults} +\section{Handling Faults}\label{sec:kernel.faulthandler} \input{../src/SEL4/Kernel/FaultHandler.lhs} -\section[vspace]{Virtual Memory} +\section{Virtual Memory}\label{sec:kernel.vspace} \input{../src/SEL4/Kernel/VSpace.lhs} -\chapter[object]{Kernel Objects} +\chapter{Kernel Objects}\label{sec:object} This chapter defines the first-class kernel objects, including their representation in physical memory, and the operations that may be performed on them by user-level threads and by other kernel-level code. -\section[structures]{Data Structures} +\section{Data Structures}\label{sec:object.structures} \input{../src/SEL4/Object/Structures.lhs} -\section[tcb]{Thread Control Blocks} +\section{Thread Control Blocks}\label{sec:object.tcb} \input{../src/SEL4/Object/TCB.lhs} -\section[cnode]{Capability Nodes} +\section{Capability Nodes}\label{sec:object.cnode} \input{../src/SEL4/Object/CNode.lhs} -\section[endpoint]{Synchronous Endpoints} +\section{Synchronous Endpoints}\label{sec:object.endpoint} \input{../src/SEL4/Object/Endpoint.lhs} -\section[asyncendpoint]{Asynchronous Endpoints} +\section{Asynchronous Endpoints}\label{sec:object.asyncendpoint} \input{../src/SEL4/Object/AsyncEndpoint.lhs} -\section[untyped]{Untyped Objects} +\section{Untyped Objects}\label{sec:object.untyped} \input{../src/SEL4/Object/Untyped.lhs} -\section[interrupt]{Interrupt Controller and Handler Objects} +\section{Interrupt Controller and Handler Objects}\label{sec:object.interrupt} \input{../src/SEL4/Object/Interrupt.lhs} -\section[objecttype]{Type-Specific Operations} +\section{Type-Specific Operations}\label{sec:object.objecttype} \input{../src/SEL4/Object/ObjectType.lhs} -\section[instances]{Storing Objects} +\section{Storing Objects}\label{sec:object.instances} \input{../src/SEL4/Object/Instances.lhs} -\chapter[model]{Haskell Model Details} +\chapter{Haskell Model Details}\label{sec:model} This chapter describes implementation details of the Haskell kernel. It should not be necessary to read this section to understand the API; however, it may help in understanding the way the model works. -\section[statedata]{System State} +\section{System State}\label{sec:model.statedata} \input{../src/SEL4/Model/StateData.lhs} -\section[pspace]{Physical Address Space Model} +\section{Physical Address Space Model}\label{sec:model.pspace} \input{../src/SEL4/Model/PSpace.lhs} -\section[syscall]{System Calls} +\section{System Calls}\label{sec:model.syscall} \input{../src/SEL4/Model/Syscall.lhs} -\section[failures]{Failures} +\section{Failures}\label{sec:model.failures} \input{../src/SEL4/Model/Failures.lhs} -\section[preemption]{Preemption} +\section{Preemption}\label{sec:model.preemption} \input{../src/SEL4/Model/Preemption.lhs} -\chapter[machine]{Modelling the Hardware}\label{ch:code:machine} +\chapter{Modelling the Hardware}\label{sec:machine}\label{ch:code:machine} This chapter defines the interface that is used by the rest of the kernel to represent the underlying hardware. -\section[registerset]{Words and Registers} +\section{Words and Registers}\label{sec:machine.registerset} \input{../src/SEL4/Machine/RegisterSet.lhs} -\section[hardware]{Hardware Functions} +\section{Hardware Functions}\label{sec:machine.hardware} \input{../src/SEL4/Machine/Hardware.lhs} \part{Architecture-Specific Features} @@ -298,7 +344,8 @@ This chapter defines a language and interpreter that may be used for writing sim \end{impdetails} -\bibliography{defs,pubs} +\bibliographystyle{plain} +\bibliography{pubs} \end{document} diff --git a/haskell/src/SEL4/Object/CNode.lhs b/haskell/src/SEL4/Object/CNode.lhs index a6c5e01e8..7ce8528f4 100644 --- a/haskell/src/SEL4/Object/CNode.lhs +++ b/haskell/src/SEL4/Object/CNode.lhs @@ -221,7 +221,7 @@ The function "invokeCNode" dispatches an invocation to one of the handlers defin > ReplyCap { capReplyMaster = False } -> cteMove cap srcSlot destSlot > _ -> fail "caller capability must be null or reply" -\subsection[ops]{CNode Operations} +\subsection{CNode Operations} The following functions define the operations that can be performed by a CNode invocation. @@ -368,7 +368,8 @@ Determine whether the CTE is valid, and has children to be deleted. If a child i > preemptionPoint > cteRevoke slot -\subsubsection[delete]{Deleting Capabilities} +\subsubsection{Deleting Capabilities} +\label{sec:object.cnode.ops.delete} This function deletes the capability in a given slot. If it is the last remaining capability for the given object, the object will be destroyed. @@ -612,7 +613,8 @@ This function is used in the assertion above; it returns "True" if no reply capa > noReplyCapsFor :: PPtr TCB -> KernelState -> Bool > noReplyCapsFor _ _ = True -\subsection[mdb]{MDB Operations} +\subsection{MDB Operations} +\label{sec:object.cnode.mdb} The Mapping Database (MDB) is used to keep track of the derivation hierachy of seL4 capabilities, so all existing capabilities to an object can be revoked before that object is reused or deleted. A similar structure is used in L4Ka::Pistachio\cite{Pistachio:URL} to support that kernel's Unmap operation. diff --git a/haskell/src/SEL4/Object/Interrupt.lhs b/haskell/src/SEL4/Object/Interrupt.lhs index c97654317..f82333e19 100644 --- a/haskell/src/SEL4/Object/Interrupt.lhs +++ b/haskell/src/SEL4/Object/Interrupt.lhs @@ -49,9 +49,9 @@ The architecture-specific definitions are imported qualified with the "Arch" pre \end{impdetails} -\subsection[invoke]{Interrupt Capability Invocations} +\subsection{Interrupt Capability Invocations} -\subsubsection[control]{Interrupt Controller Capabilities} +\subsubsection{Interrupt Controller Capabilities} There is a single, global interrupt controller object; a capability to it is provided to the initial thread at boot time. Interrupt controller capabilities may be used to generate handler capabilities for specific interrupts (see \autoref{sec:object.interrupt.invoke.handler}), or to change architecture-specific interrupt controller parameters. @@ -85,7 +85,8 @@ There is a single, global interrupt controller object; a capability to it is pro > invokeIRQControl (InterruptControl invok) = > Arch.invokeInterruptControl invok -\subsubsection[handler]{IRQ Handler Capabilities} +\subsubsection{IRQ Handler Capabilities} +\label{sec:object.interrupt.invoke.handler} An IRQ handler capability allows a thread possessing it to set an endpoint which will be notified of incoming interrupts, and to acknowledge received interrupts. @@ -113,7 +114,7 @@ An IRQ handler capability allows a thread possessing it to set an endpoint which > irqSlot <- getIRQSlot irq > cteDeleteOne irqSlot -\subsection[kernel]{Kernel Functions} +\subsection{Kernel Functions} \subsubsection{Deleting IRQ Handlers} @@ -148,7 +149,8 @@ This function is called during bootstrap to set up the initial state of the inte > setIRQState IRQTimer timerIRQ > return IRQControlCap -\subsubsection[handling]{Handling Interrupts} +\subsubsection{Handling Interrupts} +\label{sec:object.interrupt.kernel.handling} This function is called when the kernel receives an interrupt event. diff --git a/haskell/src/SEL4/Object/ObjectType.lhs b/haskell/src/SEL4/Object/ObjectType.lhs index 0a67b22e2..36cbe0032 100644 --- a/haskell/src/SEL4/Object/ObjectType.lhs +++ b/haskell/src/SEL4/Object/ObjectType.lhs @@ -81,7 +81,8 @@ Other capabilities do not require modification. > deriveCap _ cap = return cap -\subsection[finalise]{Finalising Capabilities} +\subsection{Finalising Capabilities} +\label{sec:object.objecttype.finalise} Similarly, when deleting a capability, it may be necessary to change other parts of the kernel or machine state that refer to that specific capability. If the deleted capability is the last one referring to the object, it is also necessary to clean up any references to the object itself. @@ -148,7 +149,8 @@ For any other capability, no special action is required. > finaliseCap _ _ _ = return (NullCap, Nothing) -\subsection[recycle]{Recycling Capabilities} +\subsection{Recycling Capabilities} +\label{sec:object.objecttype.recycle} When an object is recycled, its final capability will be finalised (see above) to clean up any in-kernel references to the object. Then, the object and capability must both be returned to their initial states. The "recycleCap" operation, given a capability to a finalised object, re-initialises the object and returns a capability to it. @@ -407,7 +409,7 @@ New threads are placed in the current security domain, which must be the domain > archCap <- Arch.createObject t regionBase userSize > return $! ArchObjectCap archCap -\subsection[invoke]{Invoking Objects} +\subsection{Invoking Objects} The following functions are used to handle messages that are sent to kernel objects by user level code using a "Send" or "SendWait" system call. diff --git a/haskell/src/SEL4/Object/Structures.lhs b/haskell/src/SEL4/Object/Structures.lhs index f57065900..1cb100861 100644 --- a/haskell/src/SEL4/Object/Structures.lhs +++ b/haskell/src/SEL4/Object/Structures.lhs @@ -285,7 +285,7 @@ The maximum domain is derived from the configuration parameter "numDomains" \subsection{Other Types} -\subsubsection[mdbnode]{Mapping Database Node} +\subsubsection{Mapping Database Node} The mapping database consists of a tree structure for each physical page that can be mapped at user level. It is used to keep track of all diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs index 41eedc581..6a2fc8972 100644 --- a/haskell/src/SEL4/Object/TCB.lhs +++ b/haskell/src/SEL4/Object/TCB.lhs @@ -60,7 +60,7 @@ The architecture-specific definitions are imported qualified with the "Arch" pre > import qualified SEL4.Object.TCB.TARGET as Arch -\subsection[decode]{Decoding TCB Invocations} +\subsection{Decoding TCB Invocations} There are ten types of invocation for a thread control block. All require write permission for the TCB object. In addition, "SetSpace" and "Configure" operations require grant permission. Checking for appropriate permission is done by the caller (see \autoref{sec:object.objecttype}). @@ -79,7 +79,7 @@ There are ten types of invocation for a thread control block. All require write > TCBSetSpace -> decodeSetSpace args cap slot extraCaps > _ -> throw IllegalOperation -\subsubsection[exregs]{Reading, Writing and Copying Registers} +\subsubsection{Reading, Writing and Copying Registers} The kernel provides three methods for accessing the register state of a thread; they read, write, and copy the state of the invoked thread, respectively. The implementations of these methods are in \autoref{sec:object.tcb.invoke.exregs}. @@ -158,7 +158,7 @@ For both of these operations, the first argument is a flags field. The lowest bi > writeRegsArch = transferArch } > decodeWriteRegisters _ _ = throw TruncatedMessage -\subsubsection[configure]{The Configure Call} +\subsubsection{The Configure Call} The "Configure" call is a batched call to "SetPriority", "SetIPCParams" and "SetSpace". @@ -182,7 +182,7 @@ The "Configure" call is a batched call to "SetPriority", "SetIPCParams" and "Set > tcNewIPCBuffer = tcNewIPCBuffer setIPCParams } > decodeTCBConfigure _ _ _ _ = throw TruncatedMessage -\subsubsection[setprio]{The Set Priority Call} +\subsubsection{The Set Priority Call} Setting the thread's priority is only allowed if the new priority is lower than or equal to the current thread's. This prevents untrusted clients that hold untyped or TCB capabilities from performing denial of service attacks by creating new maximum-priority threads. This is a temporary solution; there may be significant changes to the scheduler in future versions to provide better partitioning of CPU time. @@ -203,7 +203,7 @@ Setting the thread's priority is only allowed if the new priority is lower than > tcNewIPCBuffer = Nothing } > decodeSetPriority _ _ = throw TruncatedMessage -\subsubsection[setipcbuf]{The Set IPC Buffer Call} +\subsubsection{The Set IPC Buffer Call} The two thread parameters related to IPC and system call handling are the IPC buffer pointer, and a capability to access the frame containing the buffer. The kernel uses the virtual address to determine the buffer's location in the frame, and also exposes it to the thread in a well-defined location; it does not necessarily ensure that the buffer frame is actually mapped at the given address. There may be architecture-defined requirements for the pointer and frame capability; typically the only requirement is that the buffer fits inside the given frame. @@ -227,7 +227,8 @@ The two thread parameters related to IPC and system call handling are the IPC bu > tcNewIPCBuffer = Just (ipcBuffer, bufferFrame) } > decodeSetIPCBuffer _ _ _ _ = throw TruncatedMessage -\subsubsection[setspace]{The Set Space Call} +\subsubsection{The Set Space Call} +\label{sec:object.tcb.decode.setspace} Setting the capability space and virtual address space roots is similar to a pair of CNode Insert operation, except that any previous root is implicitly deleted rather than causing an error, and the new roots must be valid capabilities of the appropriate types. The fault endpoint, like the result endpoint, is not checked for validity at this point; messages sent to it will be silently dropped if it is not valid. @@ -270,11 +271,11 @@ This is to ensure that the source capability is not made invalid by the deletion > tcNewIPCBuffer = Nothing } > decodeSetSpace _ _ _ _ = throw TruncatedMessage -\subsection[invoke]{Performing TCB Invocations} +\subsection{Performing TCB Invocations} > invokeTCB :: TCBInvocation -> KernelP [Word] -\subsubsection[sched]{Scheduler Operations} +\subsubsection{Scheduler Operations} The "Suspend" and "Resume" calls are simple scheduler operations. @@ -287,7 +288,7 @@ The "Suspend" and "Resume" calls are simple scheduler operations. > restart thread > return [] -\subsubsection[tc]{Thread Control Operations} +\subsubsection{Thread Control Operations} The "ThreadControl" operation is used to implement the "SetSpace", "SetPriority", "SetIPCParams" and "Configure" methods. @@ -334,7 +335,8 @@ The use of "checkCapAt" addresses a corner case in which the only capability to > buffer > return [] -\subsubsection[exregs]{Register State} +\subsubsection{Register State} +\label{sec:object.tcb.invoke.exregs} There are three operations that read or write register state. The most general is "CopyRegisters", which transfers subsets of the register state from one specified thread to another. @@ -395,7 +397,7 @@ The "ReadRegisters" and "WriteRegisters" functions are similar to "CopyRegisters > when resumeTarget $ restart dest > return [] -\subsection[domain]{Decoding Domain Invocations} +\subsection{Decoding Domain Invocations} The domain cap is invoked to set the domain of a given TCB object to a given value. diff --git a/haskell/src/SEL4/Object/Untyped.lhs b/haskell/src/SEL4/Object/Untyped.lhs index 6edcb1755..4f2bc999a 100644 --- a/haskell/src/SEL4/Object/Untyped.lhs +++ b/haskell/src/SEL4/Object/Untyped.lhs @@ -41,12 +41,12 @@ This module defines the behavior of untyped objects. \subsection{Invocation} Invocation of an untyped object retypes the memory region, possibly creating -new typed kernel objects. As shown in \autoref{fig:.derive}, the +new typed kernel objects. As shown in \autoref{fig:derive}, the retype operation will generate one or more new capabilities, which are inserted in the mapping database as children of the initial capability. These newly created capabilities will have all access rights, and other object specific fields will be initialised to some sensible value. \begin{figure}[htp] \centering \includegraphics{figures/derive} -\caption[derive]{Invoking an Untyped Object} +\caption{Invoking an Untyped Object}\label{fig:derive} \end{figure} We start by defining a simple function to align one value to a power-of-two boundard. In particular, this function aligns its first argument up to the next power-of-two specified by the second argument. From 185f22bc3cde11a823dc6a89eff1c29588607288 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Mon, 21 Jul 2014 09:38:36 +1000 Subject: [PATCH 09/13] Add license header --- src/arch/arm/machine/errata.c | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/arch/arm/machine/errata.c b/src/arch/arm/machine/errata.c index b616846a3..8006ac051 100644 --- a/src/arch/arm/machine/errata.c +++ b/src/arch/arm/machine/errata.c @@ -1,3 +1,12 @@ +/* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + */ #include #include From d02d0c968169bbc32677822cdcf5748c26b22535 Mon Sep 17 00:00:00 2001 From: Peter Chubb Date: Wed, 23 Jul 2014 13:45:20 +1000 Subject: [PATCH 10/13] Remove -march=armv6 if -mcpu is already specified in compiler options --- it breaks older gcc --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index fa9f54866..ebf801ba1 100644 --- a/Makefile +++ b/Makefile @@ -339,7 +339,7 @@ DEFINES += -DFASTPATH endif ifeq (${ARCH}, arm) -CFLAGS += -mtune=${CPU} -marm -march=${ARMV} +CFLAGS += -mtune=${CPU} -marm ASFLAGS += -mcpu=${CPU} DEFINES += -D$(shell echo ${ARMV}|tr [:lower:] [:upper:]|tr - _) ifeq (${CPU},cortex-a8) From ac1270684d71ac377a08ee63c9ad728af8eff6c6 Mon Sep 17 00:00:00 2001 From: Peter Chubb Date: Thu, 24 Jul 2014 15:04:25 +1000 Subject: [PATCH 11/13] Fix Beagle builds For the toolchain we have, armv6 is incompatible with cpu=arm1136jf-2, but with cpu-cortex-a?, arch=armv7-a is required. --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index ebf801ba1..31f3219bf 100644 --- a/Makefile +++ b/Makefile @@ -344,9 +344,11 @@ ASFLAGS += -mcpu=${CPU} DEFINES += -D$(shell echo ${ARMV}|tr [:lower:] [:upper:]|tr - _) ifeq (${CPU},cortex-a8) DEFINES += -DARM_CORTEX_A8 +CFLAGS += -march=${ARCH} else ifeq (${CPU},cortex-a9) DEFINES += -DARM_CORTEX_A9 +CFLAGS += -march=${ARCH} endif endif endif From 649d123da5ab1a2aaf920ab441b602eae0a45d4c Mon Sep 17 00:00:00 2001 From: Peter Chubb Date: Fri, 25 Jul 2014 09:51:04 +1000 Subject: [PATCH 12/13] Fix compilation errors on Cortex-A8 Different version of GCC need diffferent combinations of -mcpu -mtune= and -march to build properly for KZM (armv6) and cortex-a8 Make CFLAGS and ASFLAGS consistent, and rely on GCC knowing which arch is which wwhen told what CPU to build for. --- Makefile | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 31f3219bf..2584ca994 100644 --- a/Makefile +++ b/Makefile @@ -339,16 +339,14 @@ DEFINES += -DFASTPATH endif ifeq (${ARCH}, arm) -CFLAGS += -mtune=${CPU} -marm +CFLAGS += -mtune=${CPU} -marm -mcpu=${CPU} ASFLAGS += -mcpu=${CPU} DEFINES += -D$(shell echo ${ARMV}|tr [:lower:] [:upper:]|tr - _) ifeq (${CPU},cortex-a8) DEFINES += -DARM_CORTEX_A8 -CFLAGS += -march=${ARCH} else ifeq (${CPU},cortex-a9) DEFINES += -DARM_CORTEX_A9 -CFLAGS += -march=${ARCH} endif endif endif From eb774331e4e448f1633a051670c45bf4b14a1ba3 Mon Sep 17 00:00:00 2001 From: Peter Chubb Date: Fri, 25 Jul 2014 12:40:43 +1000 Subject: [PATCH 13/13] More compiler fixes The in-kernel-directory Makefile was trying to reset CFLAGS, and sometimes sets them to conflict with the ones set by the Kbuild system. Only set CFLAGS and ASFLAGS for standalone builds. (standalone builds are only really supported for KZM anyway). --- Makefile | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 2584ca994..0d9de5aa8 100644 --- a/Makefile +++ b/Makefile @@ -338,9 +338,12 @@ ifdef FASTPATH DEFINES += -DFASTPATH endif +# Only set CFLAGS if we're building standalone. +# common/Makefile.Flags sets NK_CFLAGS in Kbuild environments. +ifndef NK_CFLAGS ifeq (${ARCH}, arm) -CFLAGS += -mtune=${CPU} -marm -mcpu=${CPU} -ASFLAGS += -mcpu=${CPU} +CFLAGS += -mtune=${CPU} -marm -march=${ARMV} +ASFLAGS += -mcpu=${CPU} -march=${ARMV} DEFINES += -D$(shell echo ${ARMV}|tr [:lower:] [:upper:]|tr - _) ifeq (${CPU},cortex-a8) DEFINES += -DARM_CORTEX_A8 @@ -355,6 +358,7 @@ ifeq (${ARCH}, ia32) CFLAGS += -m32 -mno-mmx -mno-sse ASFLAGS += --32 endif +endif ifeq (${CPU}, arm1136jf-s) DEFINES += -DARM1136_WORKAROUND