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

[Keunhong Lee]

Hi!

My name is Keunhong.
I'm working network systems, but I recently try to adopt formal methods on
my field.

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?

Thanks in advance!
Keunhong
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181102/f43a8034/attachment.html>