Status
The state of the system in this build: each of the 21 properties in the words of its document, with the evidence items and the gaps that name it; then all 100 gaps and the next steps. A gap is a part of the design that the code does not do yet.
Properties
The status is the column "Status" of the summary of the properties. An evidence item or a gap names a property when its text says "property <n>" or "P<n>".
Read from docs/PROPERTIES.md and docs/FIRST_MILESTONE.md.
Gaps
| Gap | Group | What the code does not do |
|---|---|---|
| 1 | A fault at the return to a program is a fault of the kernel (Review 10): the kernel refuses the one known cause (a thread whose entry or stack is not an address of a program), but any other state of a thread that the processor refuses at iretq would stop the machine. To do: treat a fault at that instruction as a fault of the program. | |
| 2 | Against the properties and the module contract | The SSE2 forms (docs/SIMD.md) are measured on the host only, at a load of 10: their speed on the machine is not measured yet. The horizontal gradient stays scalar. No AVX2 form: the kernel does not save the extended state, and the AVX2 forms that were written lost to SSE2 on the host. |
| 3 | Against the properties and the module contract | Property 19 is not complete: the description has no floats, no text of a variable size in a record, no record in a record, and no handle in a result. |
| 4 | Against the properties and the module contract | Tables as parameters (417 to 428): the console cannot call an export with an Append table or with Bytes that change (the language has no second result), and kerneltool call gives tables to read only. A record of a table has no Handle. The direct call checks nothing: a caller in the same address space that gives a count larger than its memory makes the export read past it, as with any address; only the isolated call checks. In a lent memory object the callee can write each byte of the object while the call runs, not only the table: the granularity is the object; only a call host takes this form, a service refuses it. The receiver checks overlap between parameters, not between the records of one parameter that name bytes of another (two packets of seal on the same bytes). The call region is shared during the call: an export that checks a value of a record and uses it later copies it first (as for a Text, choice 186). The console starts call hosts with its own code, not with system.call_host_start. The kernel gives each mapping that chooses no address a new range and never reuses one: a program that maps memory at each call with no address grows its page tables until its budget refuses (421 works around it in the receiver; the kernel is not changed; the fault is given to the agent of work/scheduler). The measures of 427 ran at a load of the host of 32 to 48. |
| 5 | Against the properties and the module contract | interface_module refuses an element larger than its element frame: 64 draw records or 4096 bytes of text in one element call. |
| 6 | Against the properties and the module contract | The interface package is a module for one program only (interface_through_module); the elements that take input (a button, a list, a text input) are not exports: they need the interface state of the program as a table of one row with the direction Change. |
| 7 | Against the properties and the module contract | Information functions: the catalog is the boot image and the replacement table: the module store does not exist. The error record of a malformed module gives the kind of the problem and its byte; problem(name) gives the sentence. manual reads the module records with the machine and the right Inspect, which also shows the state of each program: no grant gives the module records only. A row holds a hash as 64 hexadecimal digits, 32 bytes more than the hash; a signature longer than 112 bytes ends with "...". A function that answers about all the modules checks each file each time, with no cache: the measure includes it. The functions trust the hash of the entry of the boot image: they do not compute the hash of each file. The console keeps 256 KiB of tables for one line and 32 KiB in a variable, and a record that join makes has 256 bytes at most: columns chooses fewer fields. where compares for equality only. The module records come from the kernel, so running() shows a module that a program maps by itself only if its loader wrote a record (gap of choice 165). |
| 8 | Against the properties and the module contract | Imports and replacements: the replacement table binds the loaders of the system: the root service, the console, the call host. A program that maps code by itself can ignore it: the kernel does not check what a program does with its own memory. A module record is what the loader asserts: a program writes and removes the records of its own program, and the kernel does not compare them with the memory. A change of the table does not reach a program that runs: the root service does not start a program again. The loader finds a module only in the boot image, and the person names a module of the table by its name there: the module store does not exist. The check cannot prove that the module of a replacement behaves as the module that it replaces, and no principal signs the table (P9). A module has 8 imports at most, a program 16 modules at most, the table 32 records. A load error holds the first failure only, and one replacement of the path; it does not say which field of two Records differs (see MODULE_CONTRACT.md, "The error of a load"). The root service writes the error of a start on the log only: the program that asked the start receives a status. |
| 9 | Against the properties and the module contract | A direct call does not limit a Handle to the rights of its description: the module is in the program of the caller and has each handle of that program. |
| 10 | Against the properties and the module contract | Revocation: a grant has no end time. The root service cannot revoke one ring (it closes its handle after the start): to end a connection it uses Disconnect or stops a program. The person sees the grants of a program in the console only: no window shows the grants of all the programs. A grant that the root service did not make (a handle that one program gave to another) is in the kernel table only: no command shows it. |
| 11 | Against the properties and the module contract | A caller can give handles through a call ring and never send the call: the handles fill the 128 places of the table of the receiver until the caller revokes them or stops. A service with several callers needs a limit for each caller. |
| 12 | Against the properties and the module contract | program.has_ports stays true after the last Ports handle of a program closed: the change of program on a processor then reads the handle table for nothing. |
| 13 | Against the properties and the module contract | The console makes a handle only with buffer. It cannot make a handle with a part of the rights of another handle. |
| 14 | Against the properties and the module contract | A service: the root service has a list of the services that a program can call only for a program with the grant Connect (callable_of, today remote); the console connects to each service. A caller finds the file of a service only in the boot image. A call that never returns stops the one thread of a service such as paint: the person stops the call in the console (the console closes the connection) and closes the window of the service. |
| 15 | Against the properties and the module contract | A terminal shows one program, and a program has one terminal. A program that has a terminal has no surface. The terminal gives keys only: no pointer, no paste, no size of the view. The person cannot select or copy text. The terminal shows bytes as characters of one cell: no Unicode beyond the font, no wide character. The terminal of a stopped program stays until the person closes its window: no command of the console closes it. |
| 16 | Against the properties and the module contract | Only terminal has two pictures: the other programs can still show a part of a new picture with a part of the old one. |
| 17 | Against the properties and the module contract | The kernel ring of a thread has 32 records. workers still takes its tiles from a queue with a lock, not from a shared queue. |
| 18 | Against the properties and the module contract | A thread that stops in the middle of a write or a read of a shared queue stops the queue: no thread repairs the record of a thread that is not there. |
| 19 | Against the properties and the module contract | The milliseconds of the time page change at a tick, each millisecond; a finer time is system.nanoseconds(), from the cycle counter (choice 250). A deadline of a thread still has the resolution of the tick. No check compares the cycle counters of two processors. The time page has no date: the kernel does not read the clock of the machine. |
| 20 | Against the properties and the module contract | Limits: the root service gives each program the processor time of all its threads: no program of the desktop is limited below what it can use, and no command changes a limit while a program runs. A thread that another processor stops loses the count of its last part of a time slice (less than 1 ms). The scheduler passes over a thread with no time left each time it looks: with many such threads it reads them for nothing. The log limit is for each second on the tick: 100 records at the change of second can pass as two times the limit. |
| 21 | Against the properties and the module contract | A program can write, change and remove its own module records (Program_Module with program 0): the records that its starter wrote are not protected from it, and a report does not say who wrote a record. Found by the coordinator at the merge of step 34. Remove: the kernel marks each record with its writer (the program itself, or a holder of its handle), and a program cannot change a record of its starter. |
| 22 | Against the properties and the module contract | Error records (choices 227 to 241): the kernel finds the record of an operation after it failed, from the operation table, not from the check that refused. An operation whose checks change without a change of the table gives a wrong argument, or Refused; the program errors tests 10 kernel cases, not each check of each operation. These refusals give Refused with the status: the ranges of Device_Create, Memory_Physical on memory that is not contiguous, No_Memory, and a Bad_State of Handle_Give through memory. A record holds the first argument that is wrong; a table of error details gives each one, but only monitor.counts_named and the loader (Find and Read) declare it, and a kernel operation has none (the design is in MODULE_CONTRACT.md, section 8, "The table of error details": a bit of the kind of a command, not built, because it costs one instruction for each command). A call host gives no details of its load. A direct call of an export with a table of error details sets one more register, also when the caller gives none. The record of an isolated call comes from another program: the caller checks the kind and cannot prove the values. Only the storage service, the information exports of manual, the exports of monitor and math.square_root give an error record; the other exports give a negative number or nothing. The stack trace has 16 frames at most, and names a function only on the host, with the linked file: the system has no debug object (decision 5 of MODULE_CONTRACT.md). The kernel does not log the frames: the holder of the program handle reads them. |
| 23 | Against the properties and the module contract | The menu of the windows has no keys: the person needs the pointer. The launcher starts programs only: it does not bring a window to the front. Two windows with the same title have two equal lines. The scenario still has clicks and drags at fixed places inside windows that it placed itself. |
| 24 | Against the properties and the module contract | Memory_Unmap does not free a page table that became empty: the budget of the program pays for it until the program stops. |
| 25 | Against the properties and the module contract | One source gives one module: proved for one compiler on one host (the open fault "one build did not give one hash one time" is closed by 400 to 402). kerneltool repeat all 100 with the patched compiler, under a host load of 9.5 to 62 (median 26, 124 samples, 2026-11-11 13:26 to 15:29): for each of the 61 modules, 100 builds gave 1 module, 1 LLVM IR file and 1 object; 100 builds of the boot program gave 1 program and 1 object. Not proved: another version of the Odin compiler or of LLVM (the patch is for tag dev-2026-05; a new version needs the patch again, and repeat all again); another host or processor; the tree after the rebase on step 54 was checked by the full check (two builds), not by 100 builds. -thread-count:1 makes each build of a module single-threaded. The parallelism is one level up: one compiler process for each module (HANDOFF item 43). The report of the correction, with the compile time and what a deterministic order inside the compiler needs, is docs/REPRODUCIBLE_BUILD.md. |
| 26 | Against the properties and the module contract | The kernel tool keeps the frame pointers of each module that it builds (choice 237). A module that another tool built can omit them: the loader does not check, and the stack trace of such a module stops early. An import call goes through a stub that the linker adds. |
| 27 | Against the properties and the module contract | The test "a C program calls an Odin module" does not exist. |
| 28 | Against the properties and the module contract | The manual shows the modules of the boot image only: the module store does not exist. The documentation has one language. A module in C needs a description file for its documentation: the tool reads Odin sources only. |
| 29 | Against the properties and the module contract | The console has no command that ends the connection to a service. |
| 30 | Against the properties and the module contract | A thread has a home queue, but no affinity: the balance can move it at each choice of a thread. |
| 31 | Against the properties and the module contract | Scheduling strategies (choices 269 to 283): one strategy for the whole machine; no strategy that a program supplies (no verifier, no watchdog). A weight is for a thread, not for a budget: a program with more threads has more share. The balance counts threads, not weights: two threads of one weight in two queues with different weights get different shares. Round robin has no wake preemption (it is the reference). A wake preemption is decided under the run lock and acted on after it: if the home runs another thread when the interrupt comes, that thread loses its turn. A thread of another program preempts a processor at most once in each millisecond; a program can still make the threads of other programs pay that one preemption in each millisecond on each processor (about 2 us in the kernel each, measured), and a program whose threads wake each other preempts its own threads with no limit. The tick ends a turn under the fair strategy and EEVDF when another thread is in the queue, also a thread whose budget has no time in this period: then the pick gives the same thread again, a pass through schedule for nothing. A count of the threads that can run is not kept: a budget becomes spent with no event on the queue, so the count would need a walk of the queue at each tick, which the pick already does. The hint look_first holds one queue: a second wake before the pick replaces it. A change of strategy resets the virtual time and the lag of each thread: a program with the right Schedule that changes often moves each thread by up to one bound (3 ms, or two requests) at each change. A request of 1 us gives a new deadline at each tick: more switches, paid by the budget of the thread. A pick reads the whole queue: no measure with long queues. The delay of a wake is measured at a deadline, on the tick of 1 ms. The numbers are from one run; the test asserts no speed. Tested under QEMU with 4 processors only. |
| 32 | Against the properties and the module contract | The virtual memory of a program (choices 432 to 442): an object whose parts have their own protection is not shared (the marks are of the object). W1 (a fault through an old translation of a large page) is corrected by reading only, with no test: a test needs a fault inside the window of a shoot-down, which a program cannot make on purpose. F1' of the second read is corrected by reading only. A whole mapping of 4 KiB pages counts its present pages against the limit of one call (choice 444); a part counts each of its pages, and a part needs an object that only the program names: a part of more than 65 536 pages is several calls. The walks of a revocation, an unmap and the end of an Uncommitted object stop at the last frame or the last present entry; an object whose last page has a frame is still one pass over its slots (262 144 for 1 GiB, 2 MiB read in order, with interrupts off, under the frame lock for the release): the time is logged by address_space, not measured on a quiet host. The cases of the third read are written and not run (the coordinator builds and tests). No fault ring (a fault stops the program, as before). Decommit and the protection of a part need an object named only by the program, with one mapping. A protection change of a part of a large page is refused, not split. The map of a range of 1 GiB makes all its page tables at once (2 MiB, paid by the budget of the program), and Memory_Unmap still keeps them. The size of a large page is 2 MiB only (no 1 GiB page). The benefit of large pages was not shown: the runs were on a loaded host under KVM. The speeds of this step were all measured with a load of the host above 8. |
| 33 | Against the properties and the module contract | Frame caches (choices 348 to 354): the global exhaustion with frames in the stacks was not produced (the drain is tested by the hook of the test build, not by a real shortage); the zero at the put was not measured; a processor that only frees fills its stack and gives back by batches, a processor that only takes refills by batches, an idle processor keeps up to 256 free frames until a drain: each case is argued and seen in the counts of locks (batches taken and given differ by processor), not measured alone. Page tables and list pages still take their frames from the frame table. The rates of pages on first use were measured on a loaded host and do not show the change; the counts of the frame lock do. |
| 34 | Against the properties and the module contract | The program lock serializes the kernel entries of the threads of one program, also the word waits and wakes: over one machine test, program locks waited 1.06 million times of 18.1 million takes (memory()), mostly in programs whose threads wake each other. |
| 35 | Against the properties and the module contract | The control lock is taken by Program_State, Thread_Stop, the reports of other programs and each lent handle: a program that polls the state of another program often (monitor, a terminal) takes it each time. It waited 67 times in one machine test. |
| 36 | Against the properties and the module contract | The event of an interrupt goes to the program that held the interrupt handle when the interrupt came, read with no lock: a handle that closes at that moment can give one more event to its old owner. |
| 37 | Against the properties and the module contract | The order check costs about 10 % of a cheap kernel entry. It has no separate build without it. |
| 38 | Against the properties and the module contract | Shared code: each program that starts programs has its own table of prepared modules: two such programs that start the same module prepare it two times. A module that a program loads in itself (load in the console, the module of a call host) is not shared. A prepared module stays after its last program until the next start by the same program. The loader computes the hash of the module file at each start. |
| 39 | Against the properties and the module contract | Pages on first use: no page of zeros is shared, so the first read of a page takes a frame, as a write does. A program cannot give back the frames of a part of a memory object that lives. A memory object that is not contiguous has at most 1 GiB. |
| 40 | Against the properties and the module contract | The revocation of a mapping walks the frame list of its memory object for each word that a thread of the program waits on. Program_Report walks the page tables of the program to count its present pages. |
| 41 | Against the properties and the module contract | The 16 pages of the stack of the boot program stay in use after the kernel leaves that stack. |
| 42 | Against the properties and the module contract | With a processor that has no SMEP or SMAP, the kernel runs without these two guards. pages and the log say so. |
| 43 | Against the properties and the module contract | A reader with the grant reads the records of all the programs and all the channels: a grant for one channel does not exist. |
| 44 | Against the properties and the module contract | The boot display does not show the records of the log. A long text is cut at 80 characters in the log window. |
| 45 | Against the properties and the module contract | The boot display needs 976 x 700 pixels. On a smaller screen it is cut. |
| 46 | Against the properties and the module contract | A thread that stops with a lock held keeps the lock: the other threads wait with no end. |
| 47 | Against the properties and the module contract | The machine test failed one time in four runs of step 24 at the step that moves the window of paint ("the window paint is not at 516,408"), and passed at the next run with no change of that code. Step 27 found a cause that explains it (choice 127: the tool read a part of a line of the log) and removed it. The log of the failed run was not kept, so the cause is not proven for that run: if the failure comes again, the cause is another one. |
| 48 | Against the properties and the module contract | No QUIC, no document service, no principals, no TPM, no Secure Boot. |
| 49 | Against the properties and the module contract | The developer tool inspect (choices 316 to 324): it reads no byte of another program (no such right yet), and the stop report through Inspect hides the frames out of a module. A program that stopped has no mapping: the kernel ended them, so the map of a stopped program is empty and only its stop report and its modules stay. The fields of the scheduler of a thread are read with no run lock. The tool shows the first 11 mappings in its table and the first threads that fit; the exports give all. It names a function only when it is an export ("near"): the system has no debug object. It does not show the handles of a program, its budget in a picture, or the counters of the processor (item 94 (4) of HANDOFF.md). |
| 50 | Against the properties and the module contract | Calls from the host (choices 252 to 262): UDP has no authentication. A machine on the link of the machine that sends a datagram from 10.0.2.2 port 7100 makes a call with the grant of the remote service, which acts for the person, and reads the answer if it sees the frames. The grant of one remote filters the address; it does not prove it. QUIC, a later step, gives authentication; this step adds no password, because a secret in a datagram with no encryption protects nothing. The person can revoke the grant person, or stop remote. |
| 51 | Against the properties and the module contract | Calls from the host: a call request is one datagram, so the bytes of the arguments are 1368 at most. The host gives Integers and Texts only: no Record argument (no text form yet) and no Handle (a handle of the host names nothing in the machine). The remote service runs one call at a time, keeps the last answer only, and has 8 connections. The peer gives each answer to the program that sent the last call request: two programs of the host that call at the same time get each other's datagrams, and each one drops the parts of another number. The tool reads build/modules: a machine of another build refuses each call by its hash. The window of remote names an export by its number. Most checks of the test are still .Wait on the serial port; 11 are steps Record. The presses before remote runs, and on the machines with no remote, are not confirmed. The compositor and the log serve a call between two frames or two reads of the log: a call waits for the end of a frame. |
| 52 | Against the properties and the module contract | Network: the address is static in the network service (10.0.2.15/24, the gateway 10.0.2.2): no DHCP. A grant names an address, not a name: no DNS. No IPv6, no fragment (a fragment that arrives is refused), no IPv4 option in a frame that the network service writes, no ICMP message but echo (no "port unreachable"). |
| 53 | Against the properties and the module contract | Network: the network service writes the headers of UDP and IPv4 for each program (choice 194), and checks the ports and the checksum of each TCP segment (299): TCP is in the program, QUIC is a plan. The network service is on the data path, with one copy, because the device has one pair of queues. |
| 54 | Against the properties and the module contract | Network: one endpoint for each program, one remote for each grant, 8 endpoints, 128 Receive places in flight for each endpoint. A listen grant receives from any remote and answers only the admitted ones (297); it names no address or range of addresses that it accepts. The grant comes from the name of the program in code (endpoint_of); the person cannot give a new grant while a program runs, only revoke it. |
| 55 | Against the properties and the module contract | Network: the table of hardware addresses (16 places) learns only the answer to a request of the network service (choice 206), but a machine of the link can still answer such a request before the gateway: no ARP frame is signed. An entry stays until the table is full. One ARP request, no retry, 1000 ms for an answer. |
| 56 | Against the properties and the module contract | Network: a datagram that arrives when no Receive waits is lost (Statistics counts it). The frame service uses one message interrupt for its two queues and does not ask the device for fewer interrupts. The network device reaches all the memory of the machine, as a disk (no IOMMU). |
| 57 | Against the properties and the module contract | Network: the peer of the test checks the frames with a second implementation of the same rules, written in the same step; the known answers come from RFC 1071 and one IPv4 header. A handle that the network service received for an endpoint that the root service then could not announce (a full control ring) stays in its table. |
| 58 | Against the properties and the module contract | TCP (295 to 309): no window scaling (one connection has 65 535 bytes in flight at most), no SACK, no timestamps, no TCP Fast Open, no ECN, no Nagle rule, no keepalive, no SYN cookies (a full table refuses a SYN with a RST), no path MTU discovery, no urgent data, no IPv6. The least timeout is 200 ms and TIME-WAIT is 10 s, both shorter than the RFCs, for one link. FIN-WAIT-2 ends after 20 s (fetch aborts after 2 s). A segment to a port of no endpoint, and a segment of a remote that sent no SYN to a listen port, are dropped and counted: the network service sends no RST for them. server reads one request at a time: a second request in the same segment is lost (no pipelining). |
| 59 | Against the properties and the module contract | TLS (466): no HelloRetryRequest (a server that asks for another group fails the handshake), no session resumption, no client certificate in this layer, no X.509. The transport (468) checks the values of the transport parameters. |
| 60 | Against the properties and the module contract | QUIC on the network (506 to 517): no stateless reset; a flood that outruns one pass of quic_echo fills its places for datagrams and the network service drops real datagrams too; a flood above a shared budget (24 MB/s of Initials with no token) stops new clients while it lasts (a budget for each source prefix is designed, not built); a host with real addresses holds 2 records in the handshake of each of its addresses; a NAT rebinding ends a connection; the key of quic_echo changes at each start; remote is not over QUIC yet, and the machine does not authenticate its clients (no principals). |
| 61 | Against the properties and the module contract | QUIC transport (468): a fixed congestion window, one stream, no key update, no Version Negotiation, no Retry, no stateless reset; a NEW_CONNECTION_ID with Retire Prior To above 0 closes the connection; packets of a level whose keys are not ready are dropped; a handshake ends after 10 s. |
| 62 | Against the properties and the module contract | Cryptography (460 to 462): no hardware AES or SHA (AES-128-GCM is 4.6 times slower than ChaCha20-Poly1305 in the portable code); no batch export until tables as parameters are merged; the arithmetic of the origin has no independent review (its README says so), only the RFC vectors. |
| 63 | Against the properties and the module contract | Randomness (403 to 405): no entropy device is driven (virtio-rng-pci of QEMU is the next layer, through random.reseed of the root service); no service gives fresh bytes to a running program; the TPM (property 17) is not a source; the jitter of the cycle counter is not measured, so it is counted as 0 bits. The output of rdseed and rdrand is not tested for quality: a wrong processor gives a wrong seed with no sign. |
| 64 | Against the properties and the module contract | TCP: a host that sends SYNs from 64 ports in less than 60 s fills the admitted remotes of a listen grant for 60 s (334); its records end in 15 s and the program releases them, so the table frees earlier when the program works. A host that keeps 24 connections open with progress keeps half the records of server. Many hosts with no SYN cookies fill the table: a SYN then gets a RST. |
| 65 | Against the properties and the module contract | Same bytes (choice 359, the open fault): with the corrections of 372 to 378, server meets the second cause of choice 359 in its own path: kerneltool repeat server gave 0, 4, 0 and 5 builds of 15 that differ across the last commits, 0 of 11 for server of master in the same path, and 0 of 11 for the same commit in another path (the module holds the path of its source). The only difference in the IR of each pair: the place of the global graphics::font among the globals, an order of the work of the compiler, not a construct of the code. A differing pair is kept: /tmp/kernel_same_bytes_server/server_ir_first.ll and server_ir_2.ll. The correction at the root is the work of work/samebytes. |
| 66 | Against the properties and the module contract | HTTP (372 to 378): storage.call has no deadline: a storage service that hangs during a put stops the loop of server. A deadline alone is not right: the call region is shared, and a late answer of the service would write over the next call; it needs a busy state of the client (or put as a state machine of the loop). A Release that finds releases_waiting full is counted and lost: the network service frees its place after 120 s with no segment. |
| 67 | Against the properties and the module contract | HTTP (341 to 346): no TLS: the network is not authenticated and not secret until the work of QUIC and TLS 1.3 (docs/NETWORK.md, "QUIC"); so PUT and DELETE stay off. No chunked request body (501), no Expect: 100-continue (the server reads the body without the interim answer), no ranges, no conditional requests, no compression, no Date (no clock of the day), no virtual hosts (Host is required, not used), no URL decoding of % in a target. A line end must be CRLF: a bare LF ends no head (the client gets 431 or 408). A page has 60 KiB at most, 16 pages. The request log writes 100 records in one second at most. The answers of one connection are one at a time: a pipelined request waits for the answer before it. |
| 68 | Against the properties and the module contract | TCP: the peer tests support/tcp against itself; the test against another implementation is libslirp only, which relays to the TCP of the host. No test runs the TCP of the system against the TCP of the host kernel directly, with no relay. |
| 69 | Against the properties and the module contract | A device reaches all the memory of the machine: the machine has no IOMMU in use, so a block service with a fault can make its device write any page. The block service checks that a request names memory of the client; the device does not check it. Property 5 names the IOMMU as a requirement on real hardware. |
| 70 | Against the properties and the module contract | A block service serves one client. The storage service is the one client of the data disk; a second client needs its own disk, or a multiplexer of block rings. |
| 71 | Against the properties and the module contract | The places of the disks on the bus are fixed in support/pci: the boot record does not give the place of the boot volume. |
| 72 | Against the properties and the module contract | The block service uses one queue of the device and one message interrupt. It does not ask the device to send fewer interrupts while many requests are in flight. |
| 73 | Against the properties and the module contract | The crash test of the persistence machines ends QEMU at a time that the tool chooses from the log; the test of a loss of power (choices 382 to 384) ends it at the write of a root. The cut of a root block is made by the tool, not by a stop of the machine. |
| 74 | Against the properties and the module contract | A revoked store: notes sees -1 at its next change and keeps nothing more; its window says it. The root service gives a store by the name of the program only. |
| 75 | Against the properties and the module contract | A store has at most 48 objects, and an object at most 32 blocks (128 KiB); the call region of a connection (64 KiB) is the true limit of one write. The disk has at most 60 stores. The tables of all stores stay in the memory of the storage service. |
| 76 | Against the properties and the module contract | The storage service does not encrypt the disk, and the TPM does not seal a key (P17). |
| 77 | Against the properties and the module contract | A store is named by the name of the program, as the root service names it: two programs with one name have one store. Principals (P21) are not in the name yet. |
| 78 | Against the properties and the module contract | The storage service serves one call at a time; one call waits for each commit (two flushes). |
| 79 | Against the properties and the module contract | The loss of power: one seeded loss for each run, at the write of a root; the images of the search are built from the writes after the last flush, which is one write at that moment (the blocks of the commit were flushed before). A loss in the middle of a large write of many blocks, and a disk that reorders the writes before a flush, give the same images (any subset): the search covers them, with no machine that makes them. The checks of an image run on the host; one image starts a machine. |
| 80 | Against the properties and the module contract | The storage service does not check, at its start, that a block has one owner or that the count of blocks of a store agrees with its table. The check of each block finds a change from outside; it does not find a fault of the service itself. |
| 81 | Against the properties and the module contract | A store keeps its entry and its table block after its last object is removed. The limit of a store is written again at each change, from the grant. |
| 82 | Against the properties and the module contract | A service must copy each Text argument that it checks, as the storage service does for a name: the call region stays writable by the caller during the call. The contract does not do it for the service. |
| 83 | Against the properties and the module contract | A damaged store (a wrong table) refuses each call: the person has no way to drop it and start a new one. |
| 84 | Against the properties and the module contract | When a block service stops while a client of it keeps its data region, the device can still finish a request in that region before the root service turns off the bus master. |
| 85 | Against the properties and the module contract | The pointer (360 to 370): a program has one shape for its whole surface, and changes it with a request; it receives the pointer only when it has the focus, so a window that is not in front keeps the last shape that it asked. The compositor draws one size: the pictures of 64 and 48 wait for a screen with twice the pixels and a scale of the compositor. Windows have no resize, so the compositor never chooses a resize shape. The order of the themes is fixed in the root service until the settings service exists. The tool reads Xcursor files only (no hyprcursor, no .cur or .ani) and scales no pixel. pointers shows the first frame of an animation. The root service computes the hash of the whole theme at each start (1.4 to 1.8 ms). The theme of the owner has smooth edges against section 2 of DESIGN.md: an exception that the document states. The measures of speed of this step come from runs with a load of about 30 on the host. |
| 86 | Performance | The desktop: the places of new windows are not on the grid of 8 (264). A title that is longer than its title bar is cut. The launcher lists only the programs of bar.names, not the modules of the boot image or of a store. The launcher is drawn by the compositor: it is not a program, and it has no picture of its own. |
| 87 | Performance | Programs that still have their own palette: docs/DESIGN.md, "State". |
| 88 | Performance | runtime/memory.asm has one form for each size range, chosen on one processor (AMD Ryzen 7 5800X, ERMS and FSRM): another processor can have other crossing points. The thresholds are constants of the file, not measured at the start. |
| 89 | Performance | The new places of windows are not on the grid of 8: 13 of the 19 fixed points that the main scenario presses depend on these places. With compositor.windows() (choice 289 and after) the tool can compute each point from the place of its window; then the places can move to the grid. |
| 90 | Performance | The interface package is a support package compiled in each program; one program uses it as the module interface_module (427). Three users use it compiled in; the other windows still draw by hand (the next steps of docs/INTERFACE.md). The damage by difference matches records by index: a record added in the middle damages each record after it. A surface with two pictures is drawn whole. |
| 91 | Performance | The vector font: one glyph from the glyph cache costs 3.2 times a glyph of Spleen at scale 1 over a flat color on the host, 5.3 to 5.6 times over a gradient across or a picture (docs/FONTS.md, section 5); the machine measures were taken with a host load above 8. No grid fit of each stem, no proportional font, no character outside ASCII 32 to 126. The boot display uses the default settings until the boot pass of settings. The order of the stripes of the screen is not detected. |
| 92 | Performance | The compositor keeps at most 8 damage rectangles and draws only these for each frame. With plasma open it uses about 7 % of the processor under QEMU (60 % before, with a full redraw). A program gives the part of its surface that changed with display.present_rectangle; only the users of the interface package do. |
| 93 | Performance | The extended state is saved and restored at each switch of threads, also when a processor takes again the thread that it left just now (a restore that a field "the owner of the registers" could skip; ARCHITECTURE.md, "The extended state of the processor", section 3). The kernel form of the copies of memory uses rep movsb from 65 bytes: its speed against the loop of xmm registers is not measured. |
| 94 | Performance | The extended state: AMX is not enabled (an instruction of AMX stops the program). A processor that cannot save what the first processor saves stays stopped, and the machine runs on the others. A processor with xsave and no xsaveopt gets the fxsave path, so no AVX. The area of each thread is 2688 bytes in the thread table of the kernel also on a machine with no AVX-512 (544 KiB more than with 512 bytes). The host of the tests has no AVX-512: the zmm, opmask and AVX-512 setup paths (the 2688-byte save, the layout check of the other processors, xsetbv with bits 5 to 7) did not run in a test machine; the tool tests them on a host with AVX-512 and KVM. Without AVX-512 BW the test holds the opmask registers with kmovw: 16 bits of each of the 64. The start state check of a thread does not check the low 16 bytes of xmm0 to xmm15: the compiled code of the thread used them first. The measures of this step were not run by its author. |
| 95 | Performance | display.open repeats Handle_Give until the compositor maps the ring. |
| 96 | Input | The keyboard layout is US only. |
| 97 | Input | The console line (docs/CONSOLE.md): a stop that the console does not see (a close of its window, a fault, a loss of power) loses the line that runs then; no machine case puts a loss of power inside a commit of the line history; the history store keeps the versions of the history until the next commits thin them; the completion does not complete the second argument of a call, the fields of a record variable or the common start of several names; the fuzzy match takes a bounded window, not the best one; the search shows the best 64 lines; a list in quotes of connect names the programs that run, not only the services, because the root service gives no list of its services. |
| 98 | Input | The error records of the other calls: the frame ring has no machine case that refuses (its one client, the network service, sends right requests); the block ring has one (disk). errors has no datagram case: it has no endpoint; net and fetch show the datagram refusals. A record of an isolated call, a ring completion included, comes from another program: the caller checks its kind and its unit, and cannot prove its values. |
| 99 | Input | Versions: a remove ends an object and all its versions (an explicit act of the program); the system has no bin for a removed object. A program cannot group several commits into one step that the person undoes (property 9, open). The retention rule is fixed: no setting of the person sets it. The time of a version is the time that a machine ran since the format, until the date of part 2. The refusal of a change counts a block that two clones share two times: it can come early. A table holds 39 objects now (it held 48). The engine itself has no host test: a commit needs the block service. Its corrections (drop of damaged versions, compaction in a commit, refusals of a count) are tested on the host only through the pure procedures that it calls (storage_mount) and by a model of its rule of the index; no machine test makes a damaged index, a full index, or 21590 restores. A list that goes wrong while the service runs keeps its blocks in use until the next start. The service never compares its counts in memory with a recount while it runs. After the root service lowers the limit of a store, each change that does not shrink the store enough is refused; a remove still works. |
| 100 | Input | The date: from the real-time clock, which a person with the machine can set to any date; read each 10 s, so the date moves by the drift of the time of the system in 10 s; no network time, no time zone (UTC). A program that the root service did not start (a node of rings, a twin of frames) has no date page. The dates are 2020 to 2099 (two digits, no century register: the ACPI table FADT is not read). The grant of the two ports of the clock lets date write any byte of the memory of the clock: the processor cannot give a narrower grant without a change of the kernel. |
Read from docs/FIRST_MILESTONE.md.
Next steps
| Step | What and its state |
|---|---|
| 1 | Revocation of a grant: done (step 25), Review 5, processor time and log records in budgets: done (step 26). A window comes to the front by its name, for the person and for the test: done (step 27). |
| 2 | A program loads a module with imports; replacement of an import (MODULE_CONTRACT.md, "Replacement of an import"): done (steps 33 to 35, choices 160 to 171). |
| 3 | Paging, second part: pages on first use, and read-only code that programs share: done (steps 28 and 29, choices 128 to 141). |
| 4 | The kernel lock split by data, with measures: done (choices 210 to 225). |
| 5 | Scheduling strategies that the system can change while it runs (ideas of CFS, EEVDF and sched_ext): done (choices 269 to 283, docs/SCHEDULING.md). Not done: a strategy that a program supplies, a share for each budget. |
| 6 | A block device service (virtio), then the storage service, with a program that keeps its data: done (steps 30 to 32, choices 142 to 159). |
| 7 | The network: a virtio device service, then UDP, TCP, QUIC, with a server as the scenario. The first layer is done (choices 191 to 207): the frame service, the network service with ARP, IPv4, ICMP echo and UDP, endpoints with a grant of one remote. TCP is done (295 to 309): a library in the program over a segment endpoint, client grants and listen grants, the program server. Next: QUIC over datagrams (docs/NETWORK.md, "QUIC"). |
| 8 | Functions that give the information of the modules, rich and descriptive, with results that the console combines (owner, 2026-11-10; property 12): done (step 36, choices 172 to 182). |
| 9 | Errors that diagnose: an error record with each failure of the kernel, of a service and of a direct call, the load error of the loader; a stack trace in the report of a fault; a program with one case for each kind of error (owner, 2026-11-10): done (choices 227 to 241). |
| 10 | A program drives its virtual memory: reserve a range of addresses, change a protection, take pages back, large pages: done (choices 432 to 439; not done: the fault ring). Tables of records as parameters between modules: done (417 to 428). Then the counters of the processor for a program, and graphical tools that inspect memory and execution (owner, 2026-11-10). |
| 11 | The name modus in the code, the tool, the bar and the README. |
| 12 | The other gaps of this file: principals, signatures, TPM and Secure Boot, the document service, keyboard layouts. |
| 13 | The interface package, next users, in this order: inspect (a list with a filter and a choice, tables, a hex view), scheduler and server (their own card and large text), the bar, the menus and the window frames of the compositor, the cards of the boot display, then the tables of budget, rights, origin, limits, frames, imports, processors, the measures of crowd, flow, disk, then monitor, manual, notes, tally, terminal. Then the package as a module for each program: the description passes tables as parameters since 416, and interface_through_module uses it (426); the elements that take input need the interface state as a table of one row with the direction Change. |
| 14 | The extended state only at a switch of threads: done (548, 549). Next: skip the restore when a processor takes again the thread whose state its registers hold, with a measure. |
Read from docs/FIRST_MILESTONE.md.