§ Task and thread ctrl

Class inheritance

 kern/mem_space.cpp    kern/obj_space.cpp               
    + arch extensions     + obj_space-{phys,virt}.cpp   
 ┌────────────────┐    ┌─────────────────┐              
 │ Mem_space      │    │Generic_obj_space│              
 └────────────┬───┘    └┬────────────────┘              
              │         │                               
              │         │                               
        ┌─────▼─────────▼─┐                             
        │ Space           │ +Ref_cnt_obj                
        └────────┬────────┘                             
                 │                                      
        ┌────────▼────────┐                             
        │ Task            │ +Dyn_castable<Task,Kobject> 
        └─┬──────────┬────┘                             
          │          │
 ┌────────▼────┐ ┌───▼─────────┐                        
 │ Kernel_task │ │ Sigma0_task │
 └─────────────┘ └─────────────┘                             


Space : aggregates a set of address spaces
Task  : a protection domain, provides initialization and destruction
        functionality.

§ IPC overview

l4_ipc() : generic l4 object invocation, inlined. Arch specific.

                                                                                 
 call path of L4 (fiasco) ipc.
                                        ARCH DEPENDENT CODE
                                         ┌───────────────┐                       
                                         │ amd64: syscall│ invoke syscall
                                         │ arm64: svc #0 │
                                         └───────────────┘
┌────────────────────────┐  ┌─────────┐  ┌───────────────┐
│l4_ipc_*()  // ipc.h    ├──► l4_ipc()├──► syscall entry │                       
├────────────────────────┤  └─────────┘  └───────┬───────┘
│l4_ipc_call()           │                       │       
│l4_ipc_receive()        │               ┌───────▼───────┐ e.g.                  
│l4_ipc_send()           │               │vector handler │ arm_esr_entry()
│l4_ipc_send_and_wait()  │               └───────┬───────┘  └►handle_svc()
│l4_ipc_wait()           │                       │           └►do_syscall()
│l4_ipc_reply_and_wait() │               ┌───────▼───────┐
└────────────────────────┘               │syscall table  │
                                         └───────┬───────┘                       
                         ┏━━━━━━━━━━━━━━━┓       │
     /kern/syscalls.cpp  ┃sys_ipc_wrapper◄───────┘
                         ┗━━━━━━━━━━━━━━━┛
                           │
                        ┌──▼────────────────────┐
 fetch the obj ref      │ o = obj.deref(&rights)│ kern/thread_object.cpp
 and invoke             └──────┬────────────────┤                       
                           │   │  lookup_local()│ kern/obj_space-
                           │   └────────────────┘        {virt,phys}.cpp
                           │
                        ┏━━▼━━━━━━━━━━━━┓                               
                        ┃ o->invoke()   ┃         kern/ipc_gate.cpp
                        ┗━━━━━━━━━━━━━━━┛         kern/thread_object.cpp
                           │
                        ┏━━▼━━━━━━━━━━━━┓
                        ┃ do_ipc()      ┃         kern/thread-ipc.cpp
                        ┗━━━━━━━━━━━━━━━┛

extern "C" void sys_ipc_wrapper()
{
  assert (!(current()->state() & Thread_drq_ready));

  Thread *curr = current_thread();
  Syscall_frame *f = curr->regs()->syscall_frame();

  // [snap] some assertions (CFG NDEBUG)
  
  // the requested object
  Obj_cap obj = f->ref();
  // set flag?
  Utcb *utcb = curr->utcb().access(true);
  // model based testing
  curr->increment_mbt_counter();

  L4_fpage::Rights rights;
  // deref object and get caller rights
  Kobject_iface *o = obj.deref(&rights);        // lockup_local(cap(), rights)
  if (EXPECT_TRUE(o!=nullptr))
    o->invoke(obj, rights, f, utcb);
  else
    f->tag(curr->commit_error(utcb, L4_error::Not_existent));
}

§ OBJECT

each l4re task is assgined a factory object. factory object creates other objects.

§ OBJECT SPACE MANAGEMENT

§ IPC Gate

IPC GATE OBJECT (IMCOMPLETE)

class Ipc_gate : Kobject {
    friend class Ipc_gate_ctl;
    friend class Jdb_sender_list;
protected:
    Thread *_thread;
    Mword _id;
    Ram_quota *_quota;
    Locked_prio_list _wait_q;
}

§ FLESPAGE

flexpage represents a naturally aligned area of mappable space. Is used to describe resources in the sender’s address space.

map & unmap