kern.sire - plunder - Unnamed repository; edit this file 'description' to name the repository.

kern.sire (15840B)
      1 ; Copyright 2023 The Plunder Authors
      2 ; Use of this source code is governed by a BSD-style license that can be
      3 ; found in the LICENSE file.
      4 
      5 #### kern <- json
      6 
      7 ;;;; Cog MicroKernel
      8 ;;;; ===============
      9 ;;;;
     10 ;;;; Simple OS Kernel based on the Haskell IO Monad.
     11 ;;;;
     12 ;;;; This is probably not the ideal kernel paradigm in the long run,
     13 ;;;; since there's no good way to upgrade running code, but it works great
     14 ;;;; for demos.
     15 ;;;;
     16 ;;;;
     17 ;;;; Kernel State
     18 ;;;; ------------
     19 ;;;;
     20 ;;;; This implementation is in continuation passing style, where each step
     21 ;;;; passes around six values:
     22 ;;;;
     23 ;;;; -  `end`: What to do when this thread is done executing for now?
     24 ;;;;
     25 ;;;; -  `me`: What is the thread-id of the current thread?
     26 ;;;;
     27 ;;;; -  `fr`: A list of unused slots in the `sl` array.
     28 ;;;;
     29 ;;;; -  `kl`: A list of slots that house canceled requests.  They are not
     30 ;;;;          re-used until the next event.  Each event has multiple
     31 ;;;;          syscall responses.  If a slot was re-used before it's response
     32 ;;;;          was handled, then it will be handled by the wrong handler.
     33 ;;;;
     34 ;;;; -  `sl`: An array of "state slots", used for paused threads, Refs, etc.
     35 ;;;;
     36 ;;;; -  `rq`: An array of live requests to the runtime system.  These
     37 ;;;;          corespond 1-1 with the callbacks in `sl`.  For values in
     38 ;;;;          `sl` that are not pending syscalls, rq[key]=0
     39 ;;;;
     40 ;;;; This sequence of arguments is easy to remember with the mnemonic:
     41 ;;;; "End me for-real, kill self real-quick."  Don't actually do that,
     42 ;;;; though.
     43 ;;;;
     44 ;;;;
     45 ;;;; TODO: Strictness
     46 ;;;; ----------------
     47 ;;;;
     48 ;;;; In theory, we should be using strictness annotations everywhere in
     49 ;;;; this code.  We are accumulating lazy state, and that creates a lot
     50 ;;;; of useless thunks that need to be forced at the end of the event.
     51 ;;;;
     52 ;;;; However, the these space leaks are small and short-lived (because
     53 ;;;; each event is short-lived).  Using strictness annotations actually
     54 ;;;; slows things down.
     55 ;;;;
     56 ;;;; Eventually, when the interpreter is smarter, strictness annotations
     57 ;;;; should have negative overhead.  At that point, this code should be
     58 ;;;; made fully strict.
     59 
     60 
     61 ;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     62 
     63 :| sire
     64 :| stew
     65 
     66 
     67 ;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     68 
     69 typedef#ThreadId#Nat
     70 
     71 abstype#(Call a)
     72 
     73 ; A "running process".  This never returns, always invoking a callback instead.
     74 # typedef Action
     75     > List Nat ; Free Slots
     76     > List Nat ; Killed Threads (will become free at the end of the event)
     77     > Row Any  ; Slots (Refs, Vars, blocked threads, syscall callbacks)
     78     > Row Any  ; Syscalls.  The corresponding "slot" is the continuation.
     79     > Void
     80 
     81 # typedef Thread
     82     > Action    ;; What should we do when we're done?
     83     > ThreadId  ;; What thread is this?
     84     > Action
     85 
     86 ; An IO Action.  Returns a value by invoking a continuation.  Can be
     87 ; strung together to form a compound action by binding it's continuation
     88 ; to something.
     89 # typedef (Cog a)
     90     > (a > Thread) > Thread
     91 
     92 abstype#PausedCog
     93 
     94 } abstype#CogInput
     95 }
     96 } ; internally does (if (isTab e) ({cog_event} e) ({cog_crash} (cdr e)))
     97 } case CogInput of
     98 }     COG_EVENT e:(Tab Nat Any)
     99 }     COG_CRASH e:(Tab Nat Any)
    100 }
    101 } # newtype PausedCog
    102 } | PAUSED_COG m:(CogInput > PausedCog)
    103 
    104 ; {AgentCog} is functionally identical to `Cog`. It's a convention used to
    105 ; denote an agent.
    106 # typedef (AgentCog a)
    107     > (a > Thread) > Thread
    108 
    109 
    110 ;;; Basic Control Flow ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    111 
    112 > a > Thread
    113 = (DONE _ end me fr kl sl rq)
    114 | end [me fr] kl sl rq
    115 ; This is called when a thread reaches the end of its program.  This does
    116 ; nothing and never returns, it simply yields control back to the kernel.
    117 ;
    118 ; The rest of the kernel enforces the invariant that
    119 ; requests/continuations are zeros as soon as they are used/canceled.
    120 ; So, this doesn't need to do any of that.
    121 
    122 ; allocateSlot does not follow the convention.
    123 > List Nat > List Nat > Row Any > Row Any > (Nat > Thread)
    124 = (allocateSlot fr kl sl rq k)
    125 | if (0 == fr)
    126     @ key (len sl)
    127     @ sl  (rowSnoc sl 0)
    128     @ rq  (rowSnoc rq 0)
    129     | k key fr kl sl rq
    130 @ [key fr] | fr
    131 | k key fr kl sl rq
    132 
    133 > Cog ThreadId
    134 = (myThreadId k end me fr kl sl rq)
    135 | k me end me fr kl sl rq
    136 
    137 abstype#KernelState ; TODO
    138 
    139 > Cog KernelState
    140 = (getKernelState k end me fr kl sl rq)
    141 | k (end,me,fr,kl,sl,rq) end me fr kl sl rq
    142 
    143 > Cog a > Cog ThreadId
    144 = (fork act k end me fr kl sl rq)
    145 : tid fr kl sl rq < allocateSlot fr kl sl rq
    146 | act DONE (k tid end me) tid fr kl sl rq
    147 
    148 > Cog ThreadId
    149 = (prepareFork k end me fr kl sl rq)
    150 : tid fr kl sl rq < allocateSlot fr kl sl rq
    151 | k tid end me fr kl sl rq
    152 
    153 > ThreadId > Cog a > Cog ()
    154 = (finalizeFork tid act k end me fr kl sl rq)
    155 | act DONE (k 0 end me) tid fr kl sl rq
    156 
    157 > ThreadId > Cog () > Cog ()
    158 = (cancelFork tid act k end me fr kl sl rq)
    159 | if (tid == me)
    160     | todo {cancelfork should support canceling the current thread}
    161 @ sl | put sl tid 0
    162 @ rq | put rq tid 0
    163 | act DONE (k 0 end me) tid fr kl sl rq
    164 ; Replaces a running thread with a new action.  This is equivalent to
    165 ; (cancel+fork) except that the new code is run on the same thread as
    166 ; the old code (this is unsafe in the case where the current event has
    167 ; a response in-flight on this thread.  Only use this if that case
    168 ; is impossible).
    169 
    170 > ThreadId > Cog ()
    171 = (cancel tid k end me fr kl sl rq)
    172 @ sl (put sl tid 0)
    173 @ rq (put rq tid 0)
    174 @ kl [tid kl]
    175 | if (tid == me)                                      ; If we cancel ourselves,
    176     | end fr kl sl rq                                 ; do not continue.
    177 | k 0 end me fr kl sl rq                              ; Otherwise, continue
    178 ;
    179 ; Note that canceling a thread adds the slot to the "killed" list instead
    180 ; of the free list.  Because we have multiple syscall returns per-event,
    181 ; a canceled thread may receive a syscall response.  We need to make sure that
    182 ; these response are dropped, instead of being sent to the wrong thread.
    183 ;
    184 
    185 
    186 ;;; Refs ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    187 
    188 abstype#(Ref a)
    189 
    190 > a > Cog (Ref a)
    191 = (newRef val k end me fr kl sl rq)
    192 | if (0 == fr)
    193     @ key (len sl)
    194     @ sl  (rowSnoc sl val)
    195     @ rq  (rowSnoc rq 0)
    196     | k key end me fr kl sl rq
    197 @ [key fr] | fr
    198 @ sl       | put sl key val
    199 | k key end me fr kl sl rq
    200 
    201 > Ref a > Cog a
    202 = (readRef key k end me fr kl sl rq)
    203 | k (get sl key) end me fr kl sl rq
    204 
    205 > Ref a > a > Cog ()
    206 = (writeRef key val k end me fr kl sl rq)
    207 @ sl (put sl key val)
    208 | k 0 end me fr kl sl rq
    209 
    210 > Ref a > (a > a) > Cog ()
    211 = (modifyRef key fun k end me fr kl sl rq)
    212 @ sl (| put sl key | fun | get sl key)
    213 | k 0 end me fr kl sl rq
    214 
    215 > Ref a > Cog ()
    216 = (freeRef key k end me fr kl sl rq)
    217 @ sl (put sl key 0)
    218 @ fr [key fr]
    219 | k 0 end me fr kl sl rq
    220 
    221 
    222 ;;; MVar ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    223 
    224 abstype#(MVar a) ; TODO: #data should create this
    225 
    226 # data (MVar a)
    227 - FULL
    228     * val     : a
    229     * writers : (Row (ThreadId, a))
    230 - EMPTY
    231     * readers : Row ThreadId
    232 
    233 > a > Cog (MVar a)
    234 (newMVar val)=(newRef (**FULL val []))
    235 
    236 > Cog (MVar a)
    237 newEmptyMVar=(newRef (**EMPTY []))
    238 
    239 > MVar a > a > Cog ()
    240 = (putMVar key newVal k end me fr kl sl rq)
    241 # case (get sl key)
    242 - FULL existingVal writers
    243     @ writers | rowSnoc writers [me newVal]
    244     @ sl      | put sl key (**FULL existingVal writers)
    245     @ sl      | put sl me k
    246     | end fr kl sl rq
    247 - EMPTY readers
    248     | if (null readers)
    249         @ sl (put sl key (**FULL newVal []))
    250         | k 0 end me fr kl sl rq
    251     | else
    252         @ mvSt | (**EMPTY (drop 1 readers))
    253         @ sl   | put sl key mvSt
    254         @ them | get readers 0
    255         @ !exe | get sl them
    256         | exe newVal (k 0 end me) them fr kl sl rq
    257 
    258 > MVar a > Cog a
    259 = (takeMVar key k end me fr kl sl rq)
    260 # case (get sl key)
    261 - EMPTY readers
    262     @ mvSt | (**EMPTY (rowSnoc readers me))
    263     @ sl   | put sl key mvSt
    264     @ sl   | put sl me  k
    265     | end fr kl sl rq
    266 - FULL val writers
    267     | if (null writers)                               ; no writers, empty it
    268         @ mvSt | (**EMPTY [])
    269         @ sl   | put sl key mvSt
    270         (k val end me fr kl sl rq)
    271     | else                                            ; writers, pop first in
    272         @ them,vl | idx 0 writers                     ; queue
    273         @ writers | drop 1 writers
    274         @ mvSt    | (**FULL vl writers)
    275         @ sl      | put sl key mvSt
    276         @ !exe    | get sl them
    277         | exe 0 (k val end me) them fr kl sl rq
    278 
    279 
    280 ;;; The Kernel ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    281 
    282 > Call a > Cog a
    283 = (syscall request k end me fr kl sl rq)
    284 @ rq (put rq me request)
    285 @ sl (put sl me k)
    286 | end fr kl sl rq
    287 
    288 ;; {fullyReplaceCog} totally nukes the current cog, completely replacing
    289 ;; it with this new value.
    290 ;;
    291 ;; Danger!  Danger!  Danger!
    292 ;;
    293 ;; This will kill all running threads, cancel all syscall, and delete
    294 ;; all data.  If you want to preserve any of that, you need the new
    295 ;; state to include that information.
    296 
    297 
    298 > PausedCog > Cog b
    299 (fullyReplaceCog newCogValue k end me fr kl sl rq)=newCogValue
    300 
    301 ; To trace the kernel state at the end of each event, replace every
    302 ; reference to `KERNEL` below with a reference to `TRACED KERNEL`.
    303 = (TRACED KERNEL fr kl sl rq)
    304 @ cog (KERNEL fr kl sl rq)
    305 ; trk #[=cog]
    306 cog
    307 
    308 # typedef Kernel
    309   > List Nat
    310   > List Nat
    311   > Row Any
    312   > Row Any
    313   > Tab Nat Any
    314   > Void
    315 
    316 ; The final act of processing an event is to call this with three
    317 ; arguments.  That will yield control to the runtime system, which will
    318 ; then supply the final argument (`event`).
    319 ;
    320 ; TODO: Should `kl` be merged into `fr` at the end of `loop`?  I think
    321 ; I did it after the yield, just to make debugging simpler?
    322 ;
    323 > List Nat
    324 > List Nat
    325 > Row Any
    326 > Row Any
    327 > Tab Nat Any  ;;  The event
    328 > Void
    329 = (KERNEL fr kl sl rq event)
    330 | ifNot (isTab event)
    331     ; TODO: Remove this. This is no longer relevant.
    332     | die [{TODO: Crash handling is not implemented} event]
    333 @ fr | listWeld kl fr
    334 @ kl | ~[]
    335 ;
    336 ^ _ (tabToPairList event) fr kl sl rq
    337 ? (kernel_loop stream fr kl sl rq)
    338 | ifz stream                                   ; no more events, yield to
    339     | KERNEL fr kl sl rq                       ; the runtime
    340 @ [[key response] stream] stream
    341 @ exe | get sl key
    342 @ rq  | put rq key 0
    343 @ sl  | put sl key 0
    344 | ifz exe                                      ; call thread was canceled
    345      | kernel_loop stream fr kl sl rq          ; earlier in this event, ignore
    346 @ end | kernel_loop stream
    347 @ me  | key                                    ; Give the syscall response to
    348 | exe response end me fr kl sl rq              ; its callback.
    349 
    350 > Cog a > Cog b
    351 = (forever action return)
    352 : () < action
    353 | forever action return
    354 
    355 > Cog () > PausedCog
    356 = (runCog startUp)
    357 @ k   | DONE
    358 @ end | KERNEL
    359 @ me  | 0
    360 @ fr  | ~[]
    361 @ kl  | ~[]
    362 @ sl  | [0]
    363 @ rq  | [0]
    364 | startUp k end me fr kl sl rq
    365 ; We run the startup action on thread 0, and when it's done it will
    366 ; call (KERNEL fr kl sl rq) which will give control back to
    367 ; the runtime system.
    368 
    369 
    370 ;;; Sys Calls ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    371 
    372 = (EVAL tim exp)        | weld [%eval tim] exp
    373 = (EVAL1 tim f p)       | [%eval tim f p]
    374 = (EVAL2 tim f p q)     | [%eval tim f p q]
    375 = (EVAL3 tim f p q r)   | [%eval tim f p q r]
    376 = (EVAL4 tim f p q r s) | [%eval tim f p q r s]
    377 = (COG_SPIN f)          | [%cog %spin f]
    378 = (COG_REAP c)          | [%cog %reap c]
    379 = (COG_STOP c)          | [%cog %stop c]
    380 = (COG_WAIT c)          | [%cog %wait c]
    381 = (COG_ASK d c v)       | [%cog %ask d c v]
    382 = (COG_TELL c f)        | [%cog %tell c f]
    383 = COG_WHO               | [%cog %who]
    384 = (WHAT c)              | [%what c]
    385 = (RAND_BYTE x)         | [%rand 0 %byte x]
    386 = (HTTP_SERV ss)        | [%http 0 %serv ss]
    387 = (HTTP_HEAR)           | [%http 0 %hear]
    388 = (HTTP_HOLD n)         | [%http 0 %hold n]
    389 = (HTTP_ECHO r c m h b) | [%http 0 %echo r c m h b]
    390 = (SOCK_OPEN)           | [%sock 0 %open]
    391 = (SOCK_KILL h)         | [%sock 0 %kill h]
    392 = (SOCK_WAIT h)         | [%sock 0 %wait h]
    393 = (SOCK_RECV h)         | [%sock 0 %recv h]
    394 = (SOCK_SEND h b)       | [%sock 0 %send h b]
    395 = (WOCK_OPEN)           | [%wock 0 %open]
    396 = (WOCK_KILL h)         | [%wock 0 %kill h]
    397 = (WOCK_WAIT h)         | [%wock 0 %wait h]
    398 = (WOCK_RECV h)         | [%wock 0 %recv h]
    399 = (WOCK_SEND h b)       | [%wock 0 %send h b]
    400 = (TIME_WHEN)           | [%time 0 %when]
    401 = (TIME_WAIT x)         | [%time 0 %wait x]
    402 = (PORT_SIRE)           | [%port 0 %sire]
    403 = (PORT_CONNECT a p)    | [%port 0 %connect a p]
    404 = (PORT_ACCEPT p)       | [%port 0 %accept p]
    405 = (PORT_RECV p n)       | [%port 0 %recv p n]
    406 = (PORT_RECALL p n)     | [%port 0 %recall p n]
    407 = (PORT_SEND p b)       | [%port 0 %send p b]
    408 = (PORT_GIVE v)         | [%port 0 %give v]
    409 = (PORT_TAKE)           | [%port 0 %take]
    410 = (PORT_CLAIM s)        | [%port 0 %claim s]
    411 = (PORT_DEPLOY a)       | [%port 0 %deploy a]
    412 = (PORT_PUT h v)        | [%port 0 %put h v]
    413 = (PORT_GET h)          | [%port 0 %get h]
    414 = (PORT_CLOSE p)        | [%port 0 %close p]
    415 
    416 typedef#TimeStamp#Nat
    417 typedef#HttpReqId#Nat
    418 typedef#HttpStatusCode#Nat
    419 typedef#HttpStatusMsg#Bar
    420 typedef#HttpHeader#(Row (Bar, Bar))
    421 
    422 abstype#ServReq
    423 abstype#ServResp
    424 abstype#HttpReq ; TODO Define using #record
    425 
    426 abstype#(EvalResult a) ; TODO Use #data (it needs to do
    427                        ; length-coding first)
    428 
    429 # typedef PortSock Nat
    430 
    431 #* # backfill EVAL1     > Nat > (a>b) > a > Call (EvalResult b)
    432 #* # backfill EVAL2     > Nat > (a>b>c) > a > b > Call (EvalResult b)
    433 #* # backfill EVAL3     > Nat > (a>b>c>d) > a > b > c > Call (EvalResult b)
    434 #* # backfill RAND_BYTE > Nat > Call Bar
    435 #* # backfill TIME_WHEN > Call TimeStamp
    436 #* # backfill TIME_WAIT > TimeStamp > Call ()
    437 #* # backfill HTTP_SERV > (ServReq > Maybe ServResp) > Call Void
    438 #* # backfill HTTP_HEAR > Call HttpReq
    439 #* # backfill HTTP_HOLD > HttpReqId > Call ()
    440 
    441 # backfill HTTP_ECHO
    442 > HttpReqId > HttpStatusCode > HttpStatusMsg > HttpHeader > Bar > Call ()
    443 
    444 
    445 ;;; Utils ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    446 
    447 ; TODO: Hack: This doesn't belong here.
    448 = (forceUnpackEvalResult ctx res)
    449 # switch (len res)
    450 * 0 (die ({eval-timeout} ctx))
    451 * 1 (idx 0 res)
    452 * 2 (die ({eval-crash} ctx))
    453 
    454 ; parallel map (using the EVAL syscall)
    455 > Nat > (a > b) > Row a > Cog (Row b)
    456 = (pmap ms f args return)
    457 ;
    458 : resultMVars
    459     < ^ rowTraverse _ args
    460       & (arg stepReturn)
    461       : var < newEmptyMVar
    462       : tid < fork & threadExit
    463                    : myTid < myThreadId
    464                    : eRes < syscall (EVAL1 ms f arg)
    465                    @ !res | forceUnpackEvalResult {pmap} eRes
    466                    : _    < putMVar var res
    467                    | threadExit ()
    468       | stepReturn var
    469 ;
    470 : results
    471     < ^ rowTraverse _ resultMVars
    472       & (var stepReturn)
    473       : val < takeMVar var
    474       | stepReturn val
    475 ;
    476 | return results
    477 
    478 ;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    479 
    480 ^-^
    481 ^-^ MVar
    482 ^-^ FULL EMPTY
    483 ^-^ newMVar newEmptyMVar putMVar takeMVar
    484 ^-^
    485 ^-^ Cog PausedCog AgentCog
    486 ^-^ KERNEL DONE
    487 ^-^ forever
    488 ^-^ runCog syscall fullyReplaceCog
    489 ^-^ allocateSlot getKernelState
    490 ^-^
    491 ^-^ Ref
    492 ^-^ newRef readRef writeRef modifyRef freeRef
    493 ^-^
    494 ^-^ ThreadId
    495 ^-^ fork prepareFork finalizeFork
    496 ^-^ cancelFork cancel
    497 ^-^ myThreadId
    498 ^-^
    499 ^-^ pmap
    500 ^-^
    501 ^-^ EvalResult
    502 ^-^ EVAL EVAL1 EVAL2 EVAL3 EVAL4
    503 ^-^ forceUnpackEvalResult
    504 ^-^
    505 ^-^ COG_SPIN COG_REAP COG_STOP COG_WAIT COG_ASK COG_TELL COG_WHO
    506 ^-^
    507 ^-^ WHAT
    508 ^-^
    509 ^-^ RAND_BYTE
    510 ^-^
    511 ^-^ Call
    512 ^-^
    513 ^-^ ServReq ServResp
    514 ^-^ HttpReq HttpReqId HttpStatusCode HttpStatusMsg HttpHeader
    515 ^-^ HTTP_SERV HTTP_HEAR HTTP_HOLD HTTP_ECHO
    516 ^-^
    517 ^-^ SOCK_OPEN SOCK_KILL SOCK_WAIT SOCK_RECV SOCK_SEND
    518 ^-^
    519 ^-^ WOCK_OPEN WOCK_KILL WOCK_WAIT WOCK_RECV WOCK_SEND
    520 ^-^
    521 ^-^ TimeStamp
    522 ^-^ TIME_WHEN TIME_WAIT
    523 ^-^
    524 ^-^ PORT_SIRE
    525 ^-^ PORT_CONNECT PORT_ACCEPT PORT_SEND PORT_RECV PORT_RECALL PORT_CLOSE
    526 ^-^ PORT_GIVE PORT_TAKE PORT_CLAIM PORT_DEPLOY PORT_PUT PORT_GET
    527 ^-^ PortSock
    528 ^-^
	plunder Unnamed repository; edit this file 'description' to name the repository.
	Log \| Files \| Refs \| README \| LICENSE