notes: Basic memory modelHEADmain

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.