1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
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.
|
