[Iris-Club] Fwd: static or singleton variables in Iris?

[Ralf Jung]

Hi Keunhong,

> I have seen similar example of counter from the oneshot RA of 'iris from ground
> up' paper.
> As you mentioned, this example cannot stop a safe code to produce another
> counter() instance.
> To prevent this, the variable "counter" should reserve same namespace as the
> global functions.

It cannot and dos not want to, yes.

> In my use case, a type "Unique" contains an integer which is generated from a
> gobally, monotonically increasing counter.
> Then with the information that there exist two instances of Unique, u1 and u2,
> one can infer that u1.val != u2.val without the comparing them.
> In the 'counter' and 'oneshot' example, there exist multiple set of counter
> values and their increment continuation exist so that there may exist u1 and u2
> that u1.val = u2.val.
> 
> Thus, I expect that I have to change the lambdarust language to add another
> primitive such as 'static-let' that reserves a name from the global namespace.
> I also though about adopting 'main' function thus the 'counter' exists once in
> the body of the main function, however I wonder where I can still benefit from
> the theorems of Iris and LambaRust.

Yes, to model something akin to C's "static" you will need to change the
language.  You will need another piece of global state.  Next to the heap, you
have a table of statics mapping statically-allocated names to values.

Iris can handle this just fine.  You can then define a "static-mapsto" to
express ownership of a static "slot".  Since these are statically allocated, you
will have to find a way to distribute ownership: When the whole program starts,
the initial function receives ownership of the entire static table; it can then
distribute that to the modules as they get initialized.  This is not trivial,
but it actually reflects a real problem when using statics: Since these are
global shared state, you better make sure that no two libraries both think they
exclusively access the same static!

Given that you will have to reason about how a library actually has unique
access to its static, I usually find it easier to just encode such global
variables as being explicitly passed around instead of implicitly shared. YMMV.

I actually thought about adding something like this to model the global nature
of Rust's function namespace: Currently, a function calling another function
actually is a closure closing over that other function in its environment, and
we do not support mutual recursion. I'd like to change this some day, with a
global static map that can be used for both functions and static variables.
Rust's function types would then be just names referring to this global table
(very much like function pointers on the real machine), and the closure values
of lambdaRust would be only used for continuations. That would also make our
model of values more realistic: Rust values (i.e., values of some Rust type)
would also be something simple (an integer, a pointer or a function name) and
never anything composed (like a closure, product or sum).

Kind regards,
Ralf