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

[Ralf Jung]

Hi Keunhong,

sorry for the late reply, I had lost track of this email.

> I'm trying to understand monotonically increasing atomic integer (aka counter)
> in the context of RustBelt and Iris.
> In order to implement an atomic counter, its underlying integer variable should
> be bound to a specific namespace so that other programs cannot modify it.
> However, it seems RustBelt and Iris---in particular, the *Ref* keyword of Iris
> or *funref/let* keyword of lambdaRust---do not provide such a functionality.
> 
> I think any of "static local variables of a function" or "a singleton variable"
> would suffice to support atomic counters.
> May I ask if RustBelt or Iris support either of them?  Or, is there any way to
> formalize atomic counters in RustBelt or Iris?

I do not entirely follow your reasoning here.  To implement a monotonic counter
in heap_lang (the example programming language we usually use in Iris), you can
use something like

counter := fun () => let c = ref 0 in
  (fun () => !c, fun () => c <- !c + 1)

Now a client could do

let (get, inc) := counter () in
(get (), inc (), get ())

and that would return

(0, (), 1)

This counter is not safe for concurrency, but that can be easily fixed by making
turning the `inc` function into a CAS loop.

As usual in functional languages, heap_lang supports hiding state by putting it
into the environment of a closure.  This is somewhat similar to "static local
variables", except that every call of `counter ()` generates a *new* fresh
counter whereas static variables are typically globally unique.

For lambdaRust, we are generally only concerned with *safe* clients that
maintain the invariant of our type.  All of the types we verified at
<https://gitlab.mpi-sws.org/FP/LambdaRust-coq/tree/master/theories/typing/lib>
come with their own, custom invariant (akin to "monotonically increasing",
though usually more complicated).  Nothing stops unsafe, ill-typed code from
breaking the abstraction and manipulating these types against their protocol,
but the same is true in real Rust where unsafe code can `transmute` visibility
constraints away.  Safe code, however, can only perform operations like
overwriting an integer when it actually has that variable *at integer type* in
its context.  A monotonic counter would of course have a different type, and
thus cannot be directly overwritten by safe code.

I hope this helps!
Kind regards,
Ralf