under construction!

The ACADOS Kernel Interface

Douglas W. Jones
University of Iowa Department of Computer Science

General

The ACADOS kernel recognizes the following object classes

Pages, or memory objects of system dependent size.
Semaphores, or synchronization objects.
Mailboxes, or unbuffered message exchange objects.
Address Spaces, or arrays of capabilities for objects.
Threads, or process state objects.

Each of these object classes is discussed below. The kernel does not do many of the things you would expect from, say, a UNIX kernel. It does not contain device drivers and it does not handle page faults. These functions are expected to be performed by processes outside the kernel but essential to the operation of the system.

Many interactions with server processes involve sequences of kernel calls. It is expected that few applications will directly interact with servers using kernel calls; instead, the author of each server is expected to provide library routines that package the protocol which users are expected to use.

All code running under the AcadOS kernel runs under the authority of some thread running in some address space. Unless stated otherwise, pointers passed as parameters to the kernel are pointers to objects or data structures in that address space. Pointers to conventional data objects such as integers are pointers to data within page objects in the address space. Pointers to entire AcadOS objects are always page-aligned, and all AcadOS objects appear to occupy an entire page of the address space.

Many kernel calls and user level interface routines require the passing of array parameters. In all cases, these are described by three parameters

Address: The address of the first array element.
Length: The number of array intended to be manipulated.
Count: The address of a variable into which a count of the actual number of transferred array elements is placed.

Unfortunately, the kernel interface cannot assume language features such as array slices and implicit array bound parameters, nor can it assume static type checking. Thus, the caller must pass both the base and size of each buffer, and the user must receive, for each buffer passed, a specification of the number of elements actually manipulated.

Pages

Page objects provide the conventional memory resources for an ACADOS application. Most operations on page objects are performed by the CPU as it loads and stores data or fetches instructions. Page objects may be freely shared.

Page Allocation

register_to_receive( box return_box,: byte* pages_allocated, integer_size, null
cap* first_page, int pages_desired, null
);
send( box page_manager_box,: byte* pages_desired, integer_size, null
cap* return_box, 1, null
);
await_receipt()

The above sequence of kernel calls will attempt to allocate pages_desired pages, returning pages_allocated which will normally be equal to pages_desired but may be less, and returning a consecutive block of pages into the caller's address space starting at first_page and containing pages_allocated.

To alloate pages, the user's address space must contain a mailbox page_manager_box that references the memory manager, and a mailbox return_box used to receive the reply containing the allocated page(s). This communication through mailboxes allows memory management functions to be virtualized. In fact, the kernel may directly interpret messages sent to page_manager_box as kernel calls, or alternately, the page allocation function of the kernel may be implemented as a predefined thread running in the kernel address space.

The standard ACADOS programming environment provides a reserved location page_manager_box in the address space, and it provides a simplified interface procedure that uses this:

page_allocate(: cap* page_address,
unsigned int pages_desired,
unsigned int* pages_allocated
);

Newly allocated pages are always created with all access rights set.

Page Access Rights

The basic access rights are:

read -- the right to read operands from a page.
write -- the right to write operands to a page.
execute -- the right to fetch instructions from a page.

Not all combinations of access rights are guaranteed to be enforced on all machines! The possible combinations are as follows:

Mandatory Rights Combinations

All ACADOS systems must fully support these combinations:

read_write_execute
read_execute
no_access

Other Rights Combinations

Some ACADOS systems may support some of these combinations:

execute_only; if unsupported, read_execute will be substituted.
read_write; if unsupported, read_write_execute will be substitued.
read_only; if unsupported, read_execute will be substitued.

Few ACADOS systems will support these:

write_execute; if unsupported, read_write_execute will be substitued.
write_only; if unsupported, read_write will be substitued.

On systems that enforce the read_only, read_write and execute_only rights combinations, their use can substantially improve early fault detection by catching inappropriate execution of data or fetching of instructions as soon as they occur instead of letting execution continue to some later failure. On systems that do not support these rights combinations, their use in source code can provide useful commentary, but this must be done with extreme care; failures may result when code that makes careless use of these combinations is ported to machines that enforce them correctly.

For all combinations of access rights that may not be supported on some or most architectures, the guiding principle in making substitutions is that code that requests these rights should continue to operate on machines where they cannot be enforced. Thus, if a machine cannot enforce some rights restriction, the nearest enforcable rights combination that allows the same operations is used.

Semaphores

Semaphores are used to synchronize the execution of threads, using the general semaphore model formalized by Dijkstra.

Semaphore Allocation

register_to_receive( box return_box,: byte* sem_allocated, integer_size, null
cap* first_sem, int sems_desired, null
);
send( box sem_manager_box,: byte* sems_desired, count, 2*integer_size, null
cap* return_box, 1, null
);
await_receipt()

The above sequence of kernel calls will attempt to allocate sems_desired semaphores, each with the specified initial count, returning sems_allocated which will normally be equal to sems_desired but may be less, and returning a consecutive block of semaphores into the caller's address space starting at first_sem and containing sems_allocated.

To alloate semaphores, the user's address space must contain a mailbox sem_manager_box that references the semaphore manager, and a mailbox return_box used to receive the reply containing the allocated semaphore(s). This communication through mailboxes allows semaphore management functions to be virtualized. In fact, the kernel may directly interpret messages sent to sem_manager_box as kernel calls, or alternately, the semaphore allocation function of the kernel may be implemented as a predefined thread running in the kernel address space.

The standard ACADOS programming environment provides a reserved location box_manager_box in the address space, and it provides a simplified interface procedure that uses this:

sem_allocate(: cap* first_sem,
unsigned int sems_desired, count,
unsigned int* sems_allocated
);

Newly allocated semaphores are always created with all access rights set.

Semaphore Access Rights

The basic access rights are:

read -- the right to wait on or inspect a semaphore.
write -- the right to signal a semaphore.
reuse -- the right to use a semaphore more than once.

Most semaphores held in an address space will be reusable. The possiblity of restricting reuse of semaphores may be important in order to prevent untrusted correspondents from sending multiple signals.

Semaphore Operations

signal( sem s
);
wait( sem s
);
inspect( sem s,: int* count
);

When one thread executes a signal on some semaphore, this permits some process to continue after a wait operation on the same semaphore. If a process executes a wait operation before the corresponding signal, is received, the process that executed the wait is blocked. If the wait is executed after the corresponding signal, the process that executed the wait continues executing without pause. If multiple processes execute wait operations, each signal will unblock exactly one waiting process.

If processes have no priority structure, waiting processes will be unblocked in FIFO order. If processes have priority, waiting processes will be unblocked in priority order.

The inspect operation allows a process to read the count from a semaphore. If this is greater than zero, it indicates the number of wait operations that may be performed before a process is blocked. If this is negative, it indicates the number of blocked processes waiting for that semaphore to be signalled. Inspecting a newly created semaphore should return the same count it was created with.

Mailboxes

Mailboxs are used to pass messages between threads. These messages may contain data, bits and bytes copied from the pages of the sender's address space to the pages of the receiver's address space, and they may also contain capabilities copied from the sender's address space to the receiver's address space. Mailboxes provide for nonbuffered interthread communication. As such, from a synchronization viewpoint, the exchange of a message through a mailbox constitutes a rendezvous between the sending and receiving threads.

Rendezvous semantics is desirable in some contexts, but dangerous in others, for example, when an untrustworthy partners in a transaction leaves a critical process hanging awaiting a rendezvous. For example, consider a typical client server interaction, consisting of two message exchanges, corresponding to a call to the server and the return of the result. If the client does not accept the return message, the server is left hanging. For this reason, nonblocking (but still unbuffered) versions of the basic message exchange primitives are also provided.

Mailbox Allocation

register_to_receive( box return_box,: byte* boxes_allocated, integer_size, null
cap* first_box, int boxes_desired, null
);
send( box box_manager_box,: byte* boxes_desired, integer_size, null
cap* return_box, 1, null
);
await_receipt()

The above sequence of kernel calls will attempt to allocate boxes_desired mailboxes, returning boxes_allocated which will normally be equal to boxes_desired but may be less, and returning a consecutive block of mailboxes into the caller's address space starting at first_box and containing boxes_allocated.

To alloate boxes, the user's address space must contain a mailbox box_manager_box that references the mailbox manager, and a mailbox return_box used to receive the reply containing the allocated mailboxes(s). This communication through mailboxes allows mailbox management functions to be virtualized. In fact, the kernel may directly interpret messages sent to box_manager_box as kernel calls, or alternately, the mailbox allocation function of the kernel may be implemented as a predefined thread running in the kernel address space.

The standard ACADOS programming environment provides a reserved location box_manager_box in the address space, and it provides a simplified interface procedure that uses this:

box_allocate(: cap* first_box,
unsigned int* boxes_desired,
unsigned int* boxes_allocated
);

Newly allocated mailboxes are always created with all access rights set.

Mailbox Access Rights

The basic access rights are:

read -- the right to read messages from a mailbox.
write -- the right to write messages to a mailbox.
reuse -- the right to use a mailbox more than once.

Most mailboxes held in an address space will be reusable. The possiblity of restricting reuse of mailboxes is important in order to prevent untrusted servers from sending multiple replies to a single request.

Mailbox Operations

send( box channel,: byte* data, int data_length, int* data_moved,
cap* first_cap, int num_caps, int* caps_moved
);
non_blocking_send( box channel,: byte* data, int data_length, int* data_moved,
cap* first_cap, int num_caps, int* caps_moved
);
receive( box channel,: byte* data, int data_length, int* data_moved,
cap* first_cap, int num_caps, int* caps_moved
);
register_to_receive( box channel,: byte* data, int data_length, int* data_moved,
cap* first_cap, int num_caps, int* caps_moved
);
await_receipt()

When one thread executes a send and another thread executes a receive on the same mailbox, channel, data and capabilities are copied from the sender's to the receiver's address space.

The basic send and receive primitives will block until the data transfer is completed. The non_blocking_send primitive will only transfer data if a recipient is already waiting to receive the data, and will do nothing in the event there is no waiting recipient. The register_receive primitive registers a process's willingness to receive data from some mailbox without blocking that process.

A thread may only register for one nonblocking transfer at a time. If a process wishes to receive or to register for a second transfer, the process will block until the first transfer is complete. The await_receipt primitive blocks the caller until a previously registered transfer is complete. Calling await_receipt when no transfer is pending is a no-op. Note that the normal receive primitive is exactly equivalent to register_receive immediately followed by await_receipt.

The address data is the address of the first byte of the data buffer to use, in the address space of the caller's thread, and data_length gives the length of the data buffer, in terms of the smallest directly addressable memory units, usually bytes. After the transfer of data, both sender and receiver are informed of the number of bytes transferred in data_moved; after a transfer, this will be equal to the minimum data_length given by the sender or receiver.

The address first_cap is the address of the first capability in the list of capabilities to copy, in the address space of the caller's thread, and num_caps gives the number of capabilities to copy. After the transfer of capabilities, both sender and receiver are informed of the number of capabilities transferred in caps_moved; after a normal transfer, this will be equal to the minimum num_caps given by the sender or receiver.

If the caller is dealing with a trusted correspondant and the caller is certain that the caller's data and object lists are fully legal, the caller may pass null pointers to data_moved and caps_moved. In this case, the kernel will not attempt to report the indicated result of the copying operations.

The sender must have write access to channel, the box being used, and the receiver must have read access. If a thread attempts to use a box for an operation for which it does not have appropriate rights, a fault will be raised. If a user's data buffer is not entirely addressable for the fetch and store operations required to copy the buffer, a fault will be raised. If a user's object string extends beyond the end of the user's address space, a fault will be raised. In the event there is a fault, the state of the user's thread will be suspended immediately before the offending kernel call, and no partial copying of data or objects will occur.

The act of copying a capability with the reuse right causes that capability to be duplicated. The act of copying a capability with this right missing causes the capability to be moved and replaced, in the sender's address space, with a capability of type void and name none. This is only possible if the sender's address space is writable; if the sender's address space is not writable, a trap will be raised for the sender and the copy operation will not be undertaken.

Note that both received data and capabilities overwrite whatever was in the locations into which they are received, without regard to what was previously there. Thus, the receipt of capabilities may result in the loss of access to objects that were previously accessible from an address space.

Address Spaces

Address spaces, also known as capability lists, are used to hold arrays of capabilities. The conventional concept of a process in most operating systems modelled in AcadOS as a thread executing in an address space, where that address space contains page objects that hold the data and program of the process. The kernel imposes no restrictions on the type and placement of objects in an address space, but kernel users will generally establish conventions about, for example, the placement of the mailboxes used for standard input and standard output, as well as the server mailboxes for commonly used resources.

Address Space Allocation

register_to_receive( box return_box,: byte* space_size, integer_size, null
cap* space, 1, null
);
send( box space_manager_box,: byte* desired_size, integer_size, null
cap* {return_box, handler} 2, null
);
await_receipt()

The above sequence of kernel calls will attempt to allocate an address space, returning space_size which will normally be greater than or equal to desired_size but may be less if there is a problem. The allocated size may be greater than the desired size because of granularity in the allocation of address spaces. If the size returned is zero, the returned capability will be of type void and name none. If there is no error, capability for the allocated space will be saved in the caller's address space at space.

To alloate a new address space, the user's address space must contain a mailbox space_manager_box that references the mailbox manager, a mailbox return_box used to receive the reply containing the allocated mailboxes(s), and a mailbox handler used to receive messages reporting the occurance of exceptions in the newly created address space. The last two, return_box and handler must be occupy consecutive pages of the caller's address space.

communication through mailboxes allows address space management functions to be virtualized; the kernel may directly interpret messages sent to space_manager_box as kernel calls, or alternately, the mailbox allocation function of the kernel may be implemented as a predefined thread running in the kernel address space.

The standard ACADOS programming environment provides a reserved location space_manager_box in the address space, and it provides a simplified interface procedure that uses this:

space_allocate(: cap* space,
cap* handler,
unsigned int* desired_size,
unsigned int* space_size
);

Newly allocated address spaces are always created with the read and write access rights set.

Address Space Access Rights

The basic access rights are:

read -- the right to read a capability from an address space.
write -- the right to write a capability into an address space.
execute -- the right to launch a thread in an address space.

Address Space Operations

move_cap( cap* src, src_cap;
cap* dst, dst_cap;
int rights_mask; int* rights
);

The basic operation on an address space or capability list is to move a capability from one place to another, either within or between address spaces. The source and destination address spaces are specified by src and dst, capability offsets within the source and destination address space are given by src_cap and dst_cap. If either of the former are self the address space of the caller is used.

When a capability is moved from one place to another, the set of access rights for that capability may be restricted by rights_mask. This is anded with the rights field of the capability being moved, so rights not present in the mask are deleted. The actual set of rights delivered with the destination capability are returned in rights; if this is empty (zero), the destination capability will be of type void and name none.

To move a capability from an address space, the user must have read access to that address space. To move capabilities into an address space, the user must have write access to that address space. If a capability is moved that does not have the reuse right, it is replaced in the source address space with a capability of type void and name none; this operation requires the write access right to the source address space, if this right is missing, rights will be set to zero and void will be moved.

test( cap* space, object;: int* type, rights, name
);

The text operation allows a thread to probe the capability for for some object in the indicated space (possibly self), in order to learn the type, the access rights and the name (unique identifier) of the object. This may be used to determine what operations are legal on the object.

If two capabilities refer to objects of the same type, the name returned from testing one will be numerically equal to the name returned by testing the other only if the two capabilities reference the exact same object. It is possible for the names of objects of different types to be coincidentally equal.

make_void( cap* space, object;: int name
);

The make_void operation replaces the capability for some object in the indicated space (possibly self) with a capability of type void and the given name. Names of void objects may be assigned arbitrarily by the user. This is the usual way for a program to indicate to the system that it no longer has a need for some capability, but it should be noted that overwriting one capability with any other capability will have the same effect of making the first capability unreachable.

make_executable( cap* space;: int start
);

The make_executable operation sets the starting address for threads spawned from space to start. This operation requires write access to space and it makes space executable. The only part of a thread's initial state specified is the starting address of the code in that space. All other components of the thread state must usually be initialized by the code at that address.

Secondary Address Space Operations

The following operations on address spaces may be implemented either by the kernel or by standard library routines. Implementing these in the kernel may reduce the overhead of long strings of kernel calls, while implementing them in a standard library reduces the complexity of the kernel.

move_caps( cap* src, src_cap;
cap* dst, dst_cap; int num_caps; int* caps_moved
);

The operation move_caps moves a block of num_caps consecutive capabilities from the source to the destination, reporting, in the return argument caps_moved is used to report the number of non-void capabilities delivered to the destination. This is equivalent to a sequence of calls to move_cap.

move_data( cap* src, src_byte;
cap* dst, dst_byte; int num_bytes; int* bytes_moved
);

The operation move_data is analogous to move_caps, but it moves a block of consecutive data bytes between the pages of the indicated address space or spaces. It is equivalent to using using movecaps to get the capabilities for the required pages and then copying the bytes relative to the calling thread's address space.

restrict( cap* space, object;: int mask
);

The restrict operation manipulates the rights field of the capability for some object in the indicated space (possibly self). The rights associated with that capability are anded with the rights_mask. The indicated space must have read-write access. Restrict is equivalent to move_cap with the source and destination addresses the same.

Threads

Threads allow code to be executed in the context of some address space. The conventional concept of a process in most operating systems modelled in AcadOS as a thread executing in an address space, where that address space contains page objects that hold the data and program of the process. More than one thread may execute in an address space; if this is the case, the threads that share an address space have exactly the same access rights to all objects in that space.

Thread Allocation

register_to_receive( box return_box,: null, 0, null
cap* new_thread; 1; int* success
);
send( box thread_manager_box,: null, 0, null
cap* {return_box, space}; 3, null
);
await_receipt()

The above sequence of kernel calls will attempt to allocate a new thread attached to the indicated space. If there is no error, success will be one and a capability for the allocated thread will be saved in the caller's address space at new_thread. The newly created thread comes up running state. This implies that the pages containing the code to be executed must already be present in space.

The two capabilities return_box and space must occupy consecutive pages of the caller's address space. The capability return_box must be a mailbox and space must be an address space.

To allocate a new thread, the user's address space must contain a mailbox thread_manager_box that references the thread manager. Communication through this mailbox allows thread management functions to be virtualized. In fact, the kernel may directly interpret messages sent to thread_manager_box as kernel calls, or alternately, the thread allocation function of the kernel may be implemented as a predefined thread running in the kernel address space.

To create a new thread, the caller's address space must have execute access to space. If the caller does not have this right, or if something else prevents the system from allocating a new thread, success will be zero.

Even if the caller has no other rights to space, The created thread always gains read-write-execute access to its own address space, no matter what access was available to the caller of thread_allocate. In launching a new thread, the caller's capability to the new thread's address space will be deleted if the caller does not have reuse rights. Thus, it is possible to give out the capability to launch exactly one thread in an address space.

The standard ACADOS programming environment provides a reserved location thread_manager_box in the address space, and it provides a simplified interface procedure that uses this:

thread_allocate(: cap* space;
cap* new_thread;
int* success;
);

If the caller had read-write access to space, the new thread capability will be returned with all access rights set. If the caller did not have read or write access to space, the corresponding rights will be omitted on the new thread capability.

Thread Access Rights

The basic access rights for a thread are:

read -- the right to inspect the state of the thread.
write -- the right to modify the state of the thread.
execute -- the right to start and stop execution of the thread.

Thread Operations

start( cap* thread: );
stop( cap* thread: );

The start and stop operations are used to control whether a CPU may be assigned to the thread. Threads that were awaiting a signal on a semaphore or a message in a mailbox before a stop operation will resume only after both a start operation and the indicated event.

The start and stop operations require that the user have execute access to the thread.

get_state( cap* thread;: state* s; status* s
);
set_state( cap* thread;: state* s
);

The operations, get_state and set_state allow the the state of a running thread to be inspected or changed; these may be necessary to implement exception handlers, debuggers and trace utilities.

The operation, get_state requires read access to the thread, while set_state requires write access to the thread.

Thread State Manipulation

The thread status record is a read-only attribute of the thread; the status of a thread indicates whether or not it is running and if not, why not.

int status

This gives the status of the thread with regard to the start and stop operations and reports whether there has been an exception:

normal -- the thread may be scheduled.
stopped -- a stop operation was performed.
address_fault -- the stopped because of an instruction fetch, load or store operation on a virtual address that did not support this operation.
type_fault -- the thread stopped because of a kernel call with inappropriate argument types.

Additional values of this field are hardware defined; these are likely to include:

divide_fault -- the thread divided by zero.
floating_overflow
floating_underflow

int address

In the event of an address fault, this field indicates the virtual address that was referenced to cause the fault.

int state

This indicates the state of the thread from the point of view of the kernel's scheduler:

running on some CPU.
ready to be run.
waiting for a signal or message.

The arrival of a signal or message may change the state of a thread from waiting to ready even when that thread is not executable, but the thread will not enter the running state until it is made executable.

The thread state record is a read-write attribute of the thread, reflecting the contents of the CPU registers of the thread. The structure of this record depends on the machine architecture, but a standard set of macros or functions is provided to extract and manipulate certain fields of this state. These are semantically equivalent to record fields, but they are presented with a procedural interface because of the possibility that some architectures may have native formats for presenting these fields that are not compatable with the record field allocation schemes used by programming languages. These functions must include the following:

int get_pc( state* s)

set_pc( state* s; int pc)

The program counter of the thread.

int get_cc( state* s)

set_cc( state* s; int pc)

The condition codes of the thread. In the event that the host machine does not have condition codes, get_cc returns zero and set_cc is a no-op.

int get_sp( state* s)

set_sp( state* s; int pc)

The stack pointer of the thread. In the event that the host machine does not have a stack pointer, get_sp returns zero and set_sp is a no-op.

int get_gpr( state* s; int r)

set_gpr( state* s; int r, pc)

General purpose register r of the thread. The integer parameter r, specifying the register number, must be in the range min_gpr to max_gpr (inclusive). If there are no general purpose registers in the saved state, min_gpr will be one greater than max_gpr.

On some machines, general purpose registers may be used to hold the stack pointer and condition codes. If this is the case, programmers should be aware that, for example, set_sp may change the value of a general purpose register.

On some machines, the register set has a very irregular structure, with some registers devoted to one function and some to another; this irregular structure may be masked by the apparent presentation of all of these registers as if they were general purpose registers.

int get_fpr( state* s; int r)

set_fpr( state* s; int r, pc)

Floating point register r of the thread. The integer parameter r, specifying the register number, must be in the range min_fpr to max_fpr (inclusive). If there are no floating point registers in the saved state, min_gpr will be one greater than max_gpr.

Exceptions

When a thread encounters an exception, for example, if it attempts a fetch or store operation on an object that is not a page, the thread is stopped, exactly as if some other thread had performed a stop operation on it. After stopping the thread, the kernel sends a message to that thread's handler mailbox. An exception handler thread under AcadOS is a thread that is blocked awaiting messages on a mailbox used for the handler of some other thread.

The message to the exception handler contains the following informatio: