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

[Ralf Jung]

(forwarding an email that got accidentally rejected from the list)


Hi.

Thank your for your helpful reply!

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.

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.

Thanks in advance!
Keunhong.



2018년 12월 3일 (월) 오후 10:53, Ralf Jung <jung at mpi-sws.org
<mailto:jung at mpi-sws.org>>님이 작성:

    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