Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update 07-execution-model.md #7

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Update 07-execution-model.md #7

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions 07-execution-model.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ This section describes the execution model for the protocol, by defining:

The protocol defines distributed programs as ambient expressions which form a set of parallel and nested ambients and a path according to which an ambient moves. A program is executed, i.e. run, by reducing its initial ambient expression to its final state. The [execution of a program](https://en.wikipedia.org/wiki/Execution_(computing)) makes the ambient move and change its state. To capture the ambient structures and movement and to be able to verify that programs were correctly executed, we define an [execution model](https://en.wikipedia.org/wiki/Execution_model) for the protocol based on distributed logs of discrete events structured as [Merkle-DAGs](https://discuss.ipfs.io/t/what-is-a-merkle-dag/386) [[65](#68f94b)].

A log consists of discrete events, which occur and are recorded during the execution of a program. Starting from an initial state the program follows the ambient reduction rules, step-by-step, to a final state. Every ambient in the system records its events to its own log and includes a signature to prove authenticity. During this process, every ambient records its own log, which includes a signature to prove authenticity. The aforementioned Merkle-DAG structure keeps the log [partially ordered](#partial-order) and preserves [cryptographic integrity](#integrity).
A log consists of discrete events, which occur and are recorded during the execution of a program. Starting from an initial state the program follows the ambient reduction rules, step-by-step, to a final state. During this process, every ambient records its events to its own log, which includes a signature to prove authenticity. The aforementioned Merkle-DAG structure keeps the log [partially ordered](#partial-order) and preserves [cryptographic integrity](#integrity).

The state of an ambient, at any point in the execution, can be calculated from the events it has recorded in its log. It is the reductions, and in turn the events, that make ambients move and change their state. To look at it the other way around, the state of an ambient is recorded as immutable events in a distributed log. This enables us to analyze a program and its state at any given time in detail, to move back and forth between the states making, for example, [time-travel debugging](https://en.wikipedia.org/wiki/Time_travel_debugging) possible.

Expand Down Expand Up @@ -148,7 +148,7 @@ The Robust Ambients calculus' reduction rules specify that a reduction finishes

The duality is reflected in the log events by the definition that 1) there's a direct reference between the capability and co-capability events and 2) there are no other recorded events between them.

The events for co-capabilities `in` and `out` reference the matching event of the `in` and `out` capabilities. For example, executing a program `a[call[out a] | out call]` creates the event `out a` in the log of `a` followed by the matching event `out call` which refers to the previous event: `out a ← out call`. This forms the verifiable link between the request to move in or out of an ambient, the authority that the moving ambient was allowed to do so and a record that the ambient has indeed moved.
The events for co-capabilities `in_` and `out_` reference the matching event of the `in` and `out` capabilities. For example, executing a program `a[call[out a] | out_ call]` creates the event `out a` in the log of `a` followed by the matching event `out_ call` which refers to the previous event: `out a ← out_ call`. This forms the verifiable link between the request to move in or out of an ambient, the authority that the moving ambient was allowed to do so and a record that the ambient has indeed moved.

The `open` and `open_` are ordered differently than `in` and `out`. The `open` capability references the matching `open_` co-capability, e.g. `open_ ← open a`. Opening an ambient gives new capabilities to its opener. For example, when the ambient `a[in b.open_]` enters ambient `b[in_ a.open a]`, ambient `b` adopts the `open_` capability from `a`. The capabilities adopted by the opening ambient can be deduced from the `deploy` events referred to by the `open` event and its previous events. Interestingly, this leads to an observation that the only event that can refer to an `open_` event is the respective `open` event.

Expand Down