🎭 Concurrency
µFork is driven entirely by asynchronous events. There are no blocking operations. Instruction execution is efficiently interleaved, so all ongoing activities make progress concurrently.
Details
Activities are extremely cheap to create. In fact, a new activity is created to handle the processing of each event. An activity ends when the effects of the event are either committed (releasing new events) or aborted.
µFork supports dynamic memory allocation, with concurrent automatic reclamation of unreachable storage.
🦺 Safety
Activities are strongly isolated from each other. State-change is always local. Interaction occurs by generating asynchronous events. This simple design uses less logic and consumes less power to maintain coherency and prevent conflicts.
Details
µFork instructions are memory-safe. There are three primitive types of data:
- Bounded Integers
- Pointers to immutable data
- Addresses for events
There is no conversion between these types and no pointer/address arithmetic.
µFork enforces fine-grained quotas on memory, instructions, and events. These quotas can be used to prevent resource-exhaustion attacks.
🔑 Security
µFork security can be summarized as, “If you don't have it, you can't use it.” You have to know an address to generate an event for that address. The address-reference graph is the access-control graph.
Details
As mentioned under “Safety”, an address cannot be created from an Integer or Pointer. You only know addresses:
- Given to you at construction
- Received in an event
- Created by your actions
Addresses are opaque. They can only be used to generate an asynchronous event, not to access memory.
Overview
µFork is a novel machine architecture based on the Actor Model of computation. Actors are stateful objects that react to message-events. Each actor has a unique address. Each event designates the address of the actor to which it will be delivered. An actor handles events one-at-a-time, accumulating a set of effects which include:
- Creating new actors (create)
- Generating new message-events (send)
- Defining the actor's future behavior (become)
Actor creation is very cheap, just one instruction and one memory cell. Message send is equally cheap, and can extend the connectivity graph by transmitting actor addresses.
All data values in µFork are immutable. This makes them safe to share in message-events. The only mutation allowed is actor behavior replacement (become), which designates the code and data that will be used to handle future message-events.
Event handling ends with either a commit or abort. If the actor commits, the accumulated effects are applied to the system. If the actor aborts, the effects are discarded.
µFork is a realization of the ideas described in Memory Safety Simplifies Microprocessor Design, which explains the motivation and rationale in more detail.
Resources
- A tutorial is available to help you get started.
- The main project repository is github.com/organix/uFork
- An FPGA implementation is underway at github.com/organix/uFork/tree/main/fpga
- The legacy prototype is available at github.com/organix/ufork-c
- The NLnet project pages are uFork and uFork/FPGA
Project Support
The uFork project was funded through the NGI0 Entrust Fund. The uFork/FPGA project was funded through the NGI0 Core Fund. Funds established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101069594.