Thanks for all this info. My understanding is converging towards the following. Does that seem right to you?
Assumptions: single-threaded; volatile and non-volatile resources disjoint.
-
Non-volatile memory is your basic storage resource, holds what you last wrote (“strong” memory in concurrent terms, I believe), with the added complication of reading/writing parts of objects which adds the usual considerations about addressing, layout, alignment.
-
Only loads can access memory; and, by extension, opaque code that might load, such as calls and intrinsics. Whether these do load has a first over-approximation by kind-of-access attributes (
readnone,readonly,writeonly). -
As a result, accessing non-volatile memory is a “weak” type of side effect which only affects other memory-loading code. In particular, it is never a C-style, compiler-must-preserve-traces side effect (e.g. I/O). On the other hand, C-style side effects are assumed to access memory unless specified otherwise.
-
Individual allocations are separated by default (in the sense of separation logic), meaning accesses to memory are only valid when the pointer they dereference data-flows from the allocation site to the access site according to the rules of pointer-capture/“escaping”/MemorySSA. This leads to another over-approximation of opaque code behavior with kind-of-location attributes (
argmemonly,inaccessiblememonly, etc). -
Volatile memory access are C-style side effects that do not obey algebraic laws for memory (i.e. “reads give you the last value written”).
Could you please elaborate on memory and its relationship with side effects? I’m thinking specifically of this post.
With the current state of PL research it feels like we should know to think formally early by now, but even modern projects show otherwise. Heh, I guess one can dream. ^^ I hope these efforts with LLVM succeed.