Manual updates

This commit is contained in:
Tony Garnock-Jones 2022-02-24 13:25:03 +01:00
parent 79134ee6aa
commit bc5136c9e9
7 changed files with 173 additions and 144 deletions

View File

@ -1,5 +1,7 @@
# Architecture
<!--
> What is an architecture? It's the rules of the platform which are
> true on any embodiment of it, not just the one you work on today.
> These rules are aimed at programs (what are valid programs) and the
@ -7,6 +9,8 @@
> Giroux](https://twitter.com/__simt__/status/1489790925266059264),
> Feb. 2022
-->
The **[Syndicated Actor Model (SAM)](./glossary.md#syndicated-actor-model)** is at the heart of
Synit. In turn, the SAM builds upon [E-style actors](./glossary.md#e), replacing
message-exchange with eventually-consistent *state replication* as the fundamental building

View File

@ -5,7 +5,7 @@ data.
- [Preserves homepage](https://preserves.gitlab.io/)
- [Preserves specification](https://preserves.gitlab.io/preserves/preserves.html)
- [Preserves schema-language specification](https://preserves.gitlab.io/preserves/preserves-schema.html)
- [Preserves Schema specification](https://preserves.gitlab.io/preserves/preserves-schema.html)
- [Source code](https://gitlab.com/preserves/preserves) for many (not all) of the implementations
- Implementations for
[Nim](https://git.sr.ht/~ehmry/preserves-nim),
@ -55,9 +55,9 @@ dictionary, and record compound types. From the specification:
### Concrete syntax
Because Preserves' semantics are independent of its syntax, we may use different syntax for it
in different settings. Values can be automatically, losslessly translated from one syntax to
another.
Preserves offers *multiple* syntaxes, each useful in different settings. Values are
automatically, losslessly translatable from one syntax to another because Preserves' semantics
are syntax-independent.
The core Preserves specification defines a text-based, human-readable, JSON-like syntax, that
is a syntactic superset of JSON, and a completely equivalent compact binary syntax, crucial to
@ -92,7 +92,7 @@ serialization ordering of elements in sets and keys in dictionaries.
Having a canonical form means that, for example, a cryptographic hash of a value's canonical
serialization can be used as a unique fingerprint for the value.
For example, the SHA-512 digest of the canonical serializartion of the value
For example, the SHA-512 digest of the canonical serialization of the value
```preserves
<sms-delivery <address international "31653131313">
@ -109,8 +109,8 @@ is
### Capabilities
Preserves values can include *embedded references*, written as values with a `#!` prefix. For
example, a command adding `<some-setting>` to the user settings database might be sent to the
root dataspace as follows:
example, a command adding `<some-setting>` to the user settings database might look like this
as it travels over a Unix pipe connecting a program to the root dataspace:
```preserves
<user-settings-command <assert <some-setting>> #![0 123]>
@ -121,14 +121,15 @@ capability reference, `#![0 123]`, which encodes a transport-specific reference
> TODO: Link to documentation for `sturdy.prs`.
The syntax of values under `#!` differs depending on the medium carrying the message:
point-to-point transports need to be able to refer to "my references" (`#![0 `*n*`]`) and "your
references" (`#![1 `*n*`]`); multicast/broadcast media (like Ethernet) need to be able to name
The syntax of values under `#!` differs depending on the medium carrying the message.
For example, point-to-point transports need to be able to refer to "my references" (`#![0 `*n*`]`) and "your
references" (`#![1 `*n*`]`), while multicast/broadcast media (like Ethernet) need to be able to name
references within specific, named conversational participants (`#![<udp [192 168 1 10] 5999>
`*n*`]`) ; in-memory representations use direct pointers (`#!140425190562944`); and so on. In
every case, the references themselves function very similarly to Unix file descriptors: an
integer or similar that unforgeably denotes, in a local context, some complex data structure on
the other side of a trust boundary.
`*n*`]`), and in-memory representations need to use direct pointers (`#!140425190562944`).
In every case, the references themselves work like Unix file descriptors: an integer or similar
that unforgeably denotes, in a local context, some complex data structure on the other side of
a trust boundary.
When capability-bearing Preserves values are read off a transport, the capabilities are
automatically rewritten into references to in-memory proxy objects. The reverse process of
@ -138,7 +139,7 @@ rewriting capability references happens when an in-memory value is serialized fo
Preserves comes with a schema language suitable for defining protocols among actors/programs in
Synit. Because Preserves is a superset of JSON, its schemas can be used for parsing JSON just
as well as for native Preserves values. From the [schema
as well as for native Preserves values.[^you-have-to-use-a-preserves-reader] From the [schema
specification](https://preserves.gitlab.io/preserves/preserves-schema.html):
> A Preserves schema connects Preserves Values to host-language data
@ -334,14 +335,17 @@ Here's the Preserves value equivalent to the example above, expressed using the
called [Syrup](https://github.com/ocapn/syrup#pseudo-specification), reminiscent of
[`bencode`](https://en.wikipedia.org/wiki/Bencode).
[^you-have-to-use-a-preserves-reader]: You have to use a Preserves text-syntax reader on JSON
terms to do this, though: JSON values like `null`, `true`, and `false` naively read as
Preserves *symbols*. Preserves doesn't have the concept of `null`.
[^this-example-from-mdbook]: This example is a simplified form of the preprocessor type
definitions for
[mdBook](https://rust-lang.github.io/mdBook/for_developers/preprocessors.html), the system
used to render this manual. I use a real [Preserves schema
used to render these pages. I use a real [Preserves schema
definition](https://git.syndicate-lang.org/synit/synit/src/branch/main/manual/book.prs) for
parsing and producing Serde's JSON representation of mdBook `Book` structures in order to
[preprocess the manual's source
code](https://git.syndicate-lang.org/synit/synit/src/branch/main/manual/mdbook-ditaa).
[preprocess the text](https://git.syndicate-lang.org/synit/synit/src/branch/main/manual/mdbook-ditaa).
[^lose-compatibility]: By doing so, we lose compatibility with the Serde structures, but the
point is to show the kinds of schemas available to us once we move away from strict

View File

@ -1,4 +1,4 @@
# Synit: a Reactive Operating System
# Synit is a Reactive Operating System
## Welcome!
@ -14,25 +14,32 @@ familiar to Linux users, but also incorporates many ideas drawn from
programming languages and operating systems not closely connected with
Linux's Unix heritage.
It is currently **experimental** software.
- Project homepage: <https://synit.org/>
- Source code: <https://git.syndicate-lang.org/synit/>
## Organisation of this manual
<!--
This manual is organised into sections:
## Who should read these pages
1. Preliminaries. **[Architecture](./architecture.md)**, **[installation
instructions](./install.md)**, and **[project glossary](./glossary.md)**.
These pages present information about Synit for a few different audiences.
2. **[User and Administration Guide.](./operation/index.md)** The system handbook for Synit.
- To learn more about Synit and its foundations, you can read
- an overview of its [architecture](./architecture.md),
- [installation instructions](./install.md) for the system, and
- an extensive [project glossary](./glossary.md).
3. **[Programming Guide and Reference.](./guide/index.md)** How to write programs for Synit.
- For information on how to configure and use a Synit system, see the [User and Administration
Guide](./operation/index.md), a nascent system handbook for Synit.
4. **[Specifications and Theory.](./theory/index.md)** Deeper investigation of some of the
concepts underpinning Synit's architecture.
- To learn about writing programs that integrate into Synit, see the [Programming Guide and
Reference](./guide/index.md).
- Finally, the section on [Specifications and Theory](./theory/index.md) digs deeper into some
of the concepts underpinning Synit's architecture. This is also the section where you will
find formal specification of the various protocols and data structures that make Synit
interesting.
-->
## Quickstart

View File

@ -15,9 +15,9 @@ bus](./system-bus.md) (NB. not at PID 1).
| | | | | |
+--+--+ +---+---+ +--+--+ +----+----+ +---+---+ +-----+-----+
|init | |console| |udevd| |Network | |Wifi | |Session bus|
+-----+ |getty | +-----+ |Interface| |Daemon | ... +-----+-----+
+-------+ |Monitor | |(wlan0)| |
|Daemon | +-------+ |
+-----+ |getty | +-----+ |Interface| |Daemon | ... |(syndicate|
+-------+ |Monitor | |(wlan0)| | server) |
|Daemon | +-------+ +-----+-----+
+---------+ |
|
+----------+----------------------------+

View File

@ -23,7 +23,7 @@ It provides:
through the gatekeeper.
5. An [`inotify`](https://en.wikipedia.org/wiki/Inotify)-based **[configuration
loader](./builtin/config-watcher.md)** which loads and executes configuration files written
tracker](./builtin/config-watcher.md)** which loads and executes configuration files written
in the scripting language.
6. [**Process startup and supervision**](./builtin/daemon.md)

View File

@ -1,13 +1,16 @@
# Syndicate Protocol
Actors in the same local [scope](./glossary#scope) communicate directly. To communicate further
afield, scopes may be *connected* using [relay actors](./glossary.md#relay). Relays allow
Actors that share a local [scope](./glossary#scope) can communicate directly. To communicate
further afield, scopes are *connected* using [relay actors](./glossary.md#relay). Relays allow
*indirect* communication: distant entities can be addressed as if they were local.
Relays exchange *Syndicate Protocol* messages across a [transport](./glossary.md#transport). A
*transport* is the underlying medium connecting one relay to its counterparts on a given
network. For example, a TLS-on-TCP/IP socket may connect a pair of relays to one another, or a
UDP multicast socket may connect an entire group of relays across an ethernet.
UDP multicast socket may connect an entire group of relays across an
ethernet.[^relaying-over-syndicate]
<!--
```ditaa protocol-transport
+-------------+ +-------------+
@ -19,13 +22,15 @@ UDP multicast socket may connect an entire group of relays across an ethernet.
+-------------+ +-------------+
```
-->
## Transport requirements
Transports must
- be able to carry [Preserves](./glossary.md#preserves) values back and forth,
- be reliable and in-order,
- have a well-defined lifecycle (created → connected → disconnected), and
- have a well-defined session lifecycle (created → connected → disconnected), and
- assure confidentiality, integrity and replay-resistance.
This document focuses primarily on point-to-point transports, discussing multicast and
@ -328,110 +333,6 @@ The above definitions imply some *validity constraints* on `Caveat`s.
Implementations MUST enforce these constraints (either statically or dynamically).
#### Pseudocode for attenuation, pattern matching, and template instantiation
##### Attenuation
```python
def attenuate(attenuation, value):
for caveat in reversed(attenuation):
value = applyCaveat(caveat, value)
if value is None:
return None
return value
def applyCaveat(caveat, value):
if caveat is 'Alts' variant:
for rewrite in caveat.alternatives:
possibleResult = tryRewrite(rewrite, value);
if possibleResult is not None:
return possibleResult
return None
if caveat is 'Rewrite' variant:
return tryRewrite(caveat, value)
def tryRewrite(rewrite, value):
bindings = applyPattern(rewrite.pattern, value)
if bindings is None:
return None
else:
return instantiateTemplate(rewrite.template, bindings)
```
##### Pattern matching
```python
def match(pattern, value, bindings):
if pattern is 'PDiscard' variant:
return True
if pattern is 'PAtom' variant:
return True if value is of the appropriate atomic class else False
if pattern is 'PEmbedded' variant:
return True if value is a capability else False
if pattern is 'PBind' variant:
append value to bindings
return match(pattern.pattern, value, bindings)
if pattern is 'PAnd' variant:
for p in pattern.patterns:
if not match(p, value, bindings):
return False
return True
if pattern is 'PNot' variant:
return False if match(pattern.pattern, value, bindings) else True
if pattern is 'Lit' variant:
return (pattern.value == value)
if pattern is 'PCompound' variant:
if pattern is 'rec' variant:
if value is not a record: return False
if value.label is not equal to pattern.label: return False
if value.fields.length is not equal to pattern.fields.length: return False
for i in [0 .. pattern.fields.length):
if not match(pattern.fields[i], value.fields[i], bindings):
return False
return True
if pattern is 'arr' variant:
if value is not a sequence: return False
if value.length is not equal to pattern.items.length: return False
for i in [0 .. pattern.items.length):
if not match(pattern.items[i], value[i], bindings):
return False
return True
if pattern is 'dict' variant:
if value is not a dictionary: return False
for k in keys of pattern.entries:
if k not in keys of value: return False
if not match(pattern.entries[k], value[k], bindings):
return False
return True
```
##### Template instantiation
```python
def instantiate(template, bindings):
if template is 'TAttenuate' variant:
c = instantiate(template.template, bindings)
if c is not a capability: raise an exception
c = c with the caveats in template.attenuation appended to the existing
attenuation in c
return c
if template is 'TRef' variant:
if 0 ≤ template.binding < bindings.length:
return bindings[template.binding]
else:
raise an exception
if template is 'Lit' variant:
return template.value
if template is 'TCompound' variant:
if template is 'rec' variant:
return Record(label=template.label,
fields=[instantiate(t, bindings) for t in template.fields])
if template is 'arr' variant:
return [instantiate(t, bindings) for t in template.items]
if template is 'dict' variant:
result = {}
for k in keys of template.entries:
result[k] = instantiate(template.entries[k], bindings)
return result
```
## Membranes
In order to correctly map between embedded references on the wire and entity references local
@ -569,7 +470,7 @@ WebSockets
Multicast/broadcast, in-memory
## Reference: Complete schema of the protocol
## Appendix: Complete schema of the protocol
The following is a consolidated form of the definitions from the text above.
@ -641,10 +542,122 @@ TCompound =
/ @dict <dict @entries { any: Template ...:... }> .
```
## Appendix: Pseudocode for attenuation, pattern matching, and template instantiation
### Attenuation
```python
def attenuate(attenuation, value):
for caveat in reversed(attenuation):
value = applyCaveat(caveat, value)
if value is None:
return None
return value
def applyCaveat(caveat, value):
if caveat is 'Alts' variant:
for rewrite in caveat.alternatives:
possibleResult = tryRewrite(rewrite, value);
if possibleResult is not None:
return possibleResult
return None
if caveat is 'Rewrite' variant:
return tryRewrite(caveat, value)
def tryRewrite(rewrite, value):
bindings = applyPattern(rewrite.pattern, value)
if bindings is None:
return None
else:
return instantiateTemplate(rewrite.template, bindings)
```
### Pattern matching
```python
def match(pattern, value, bindings):
if pattern is 'PDiscard' variant:
return True
if pattern is 'PAtom' variant:
return True if value is of the appropriate atomic class else False
if pattern is 'PEmbedded' variant:
return True if value is a capability else False
if pattern is 'PBind' variant:
append value to bindings
return match(pattern.pattern, value, bindings)
if pattern is 'PAnd' variant:
for p in pattern.patterns:
if not match(p, value, bindings):
return False
return True
if pattern is 'PNot' variant:
return False if match(pattern.pattern, value, bindings) else True
if pattern is 'Lit' variant:
return (pattern.value == value)
if pattern is 'PCompound' variant:
if pattern is 'rec' variant:
if value is not a record: return False
if value.label is not equal to pattern.label: return False
if value.fields.length is not equal to pattern.fields.length: return False
for i in [0 .. pattern.fields.length):
if not match(pattern.fields[i], value.fields[i], bindings):
return False
return True
if pattern is 'arr' variant:
if value is not a sequence: return False
if value.length is not equal to pattern.items.length: return False
for i in [0 .. pattern.items.length):
if not match(pattern.items[i], value[i], bindings):
return False
return True
if pattern is 'dict' variant:
if value is not a dictionary: return False
for k in keys of pattern.entries:
if k not in keys of value: return False
if not match(pattern.entries[k], value[k], bindings):
return False
return True
```
### Template instantiation
```python
def instantiate(template, bindings):
if template is 'TAttenuate' variant:
c = instantiate(template.template, bindings)
if c is not a capability: raise an exception
c = c with the caveats in template.attenuation appended to the existing
attenuation in c
return c
if template is 'TRef' variant:
if 0 ≤ template.binding < bindings.length:
return bindings[template.binding]
else:
raise an exception
if template is 'Lit' variant:
return template.value
if template is 'TCompound' variant:
if template is 'rec' variant:
return Record(label=template.label,
fields=[instantiate(t, bindings) for t in template.fields])
if template is 'arr' variant:
return [instantiate(t, bindings) for t in template.items]
if template is 'dict' variant:
result = {}
for k in keys of template.entries:
result[k] = instantiate(template.entries[k], bindings)
return result
```
---
#### Notes
[^relaying-over-syndicate]: In fact, it makes perfect sense to run the relay protocol between
actors that are *already connected* in some scope: this is like running a VPN, tunnelling
IP over IP. A variation of the Syndicate Protocol like this gives [federated
dataspaces](https://syndicate-lang.org/about/history/#postdoc).
[^no-extensions-yet]: This specification does not define any extensions, but future revisions
could, for example, use extensions to perform version-negotiation. Another potential future
use could be to propagate provenance information for tracing/debugging.

View File

@ -1,5 +1,6 @@
div.ditaa {
overflow: scroll;
overflow: auto;
line-height: 0;
}
svg text {