diff options
| -rw-r--r-- | notes/memory_model.txt | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/notes/memory_model.txt b/notes/memory_model.txt new file mode 100644 index 0000000..7705684 --- /dev/null +++ b/notes/memory_model.txt @@ -0,0 +1,117 @@ +Memory model +============ + +Read/write modes: + - read-only (default) + - read/write ("var" keyword) + - write-only ("writeonly" keyword) + (-no access ("addr" keyword)) + +Sharing modes: + - unshared (default) + - shared + (- rshared) + (- wshared) + +Locations and paths +------------------- +A data location some area in memory. Multiple references may point +to the same data location. With union types, a data location can +store multiple different types of data in the same location. + +A path is a way to access a data location. It can be a direct access, +such as a local variable, or it can be indirect via references. + +Visibility +---------- +A data location is visible when it is either: +- a local variable which is in scope +- a function parameter in a function that has not finished execution +- a gloal variable +- reachable via a reference that is visible +AND there is at least one operation that uses it, that is reachable + via any series of true/false branches following the currently + executing operation (including operations in the current operation). +A visible path is a path that makes a data location visible. + +Accessibility +------------- +A data location is accessible when it is visible and any conditions and +typestates required to access it are satisfied. +An accessible path is a path that makes a data location accessible. + +There may be multiple paths to the same data location. For example, there +can be a local variable and a pointer that points to the local variable. + +Unshared read-only paths +------------------------ +When an accessible path gives unshared access to a variable, there may not be +any other accessible paths the same data location that grant write permission. + +In addition, the data location may not be modified externally, +such as by a library, by an OS function, by hardware or similar. + +Modification is disallowed, with the following exception: +- A local read-only variable must be assigned exactly once before usage +- A such write may be delayed, but must be performed before the first read + via the path (if any) and before the data location becomes accessible via + another path (if ever) [the latter always happens after the + path is no longer accessible by ourselves] + +Reads may be performed as soon as the path becomes accessible. + +Unshared read-write and write-only paths +---------------------------------------- +In this case, all other accessible paths must be shared read-only. + +An unshared read-only data location may not be read or modified externally. + +The rules for reads and local variable assignment for read-only unshared +paths apply for read-write paths also. Write-only paths may not be +written to, except for the initial assignment for local variables. + +Writes may be delayed, but must be performed before the first read +via the path (if any) and before the data location becomes accessible via +another path (if ever) [the latter always happens after the +path is no longer accessible by ourselves] + +Shared read-only paths +---------------------- +In this case, there are no restrictions on other accessible paths, +and also no restrictions on external access. + +Reads must happen in unchanged order, in relation to other shared +reads or writes, including any function calls that might perform +shared reads or writes. + +Shared read-write paths +----------------------- +In this case, there may not be any accessible unshared paths to the +same data location. + +Reads and writes must happen in unchanged order, in relation to other shared +reads or writes, including any function calls that might perform +shared reads or writes. + +Atomicity +--------- +Single read operations via shared paths must be atomic if the +type of the data item is: +1. a reference +2. a usize/ssize type +3. a byte,short,ushort,int,uint type +4. 16 bits of size or less +5. an enum with any of the above as a base type + +Single write operations via shared paths must be atomic if the +type of the data item is: +1. a reference +2. a usize/ssize type +For types in cases 3-5: Those may be implemented as a word read (non-atomic) + +modify + word write (atomic) sequence. So those are only atomic if there +are no other writers. + +Any other operations are not guaranteed to be atomic. + +Combined read-writes like += may be implemented using +a separate read and write operation. |