Rejected (valid?) integrity mismatch when lowering mailbox clearance

[ssoelvsten]

For funsies, I was tinkering with replacing nsuref.trp with a fully-fledged Ref module. The test runs into the following error at the first Ref.get when using a root authority.

Runtime error in thread 8c1f6ccd-8205-4b80-97b5-306da02b2755@{}%{}
>> Integrity level mismatch for lowering mailbox clearance
 | integrity level of the data: #root
 | integrity level of the target: #root-integrity

lib/Ref.trp

datatype Atoms = GET | SET | DEL

let (** Initialises a new shared mutable variable with value `x_init`. This is implemented by means
     *  of messages to/from a separate tail-recursive thread that updates its state. To mitigate
     *  an update cannot be sent due to the blocking label, the mailbox clearance needs to be
     *  raised by means of the given authority, `auth`.
     *)
    fun make auth x_init =
        let fun make' _ =
                let val c = raisembox(`{#ROOT}`)
                    fun loop x =
                        rcv (`{}`, `{#ROOT}`,
                              [ hn (GET, origin) => send(origin, (GET, x)); loop x
                              , hn (SET, x')     => loop x'
                              , hn (DEL)         => ()
                              ])
                    val _ = loop x_init
                    val _ = lowermbox(c, auth)
                in () end
        in spawn make' end

    (** Deinitialises the shared variable in reference `r`. After this, all calls to `get` will be
     *  blocking. *)
    fun destroy _ r = send(r, (DEL))

    (** Get the value stored in `r`. This value is blocking, if `r` has been destroyed. *)
    fun get auth r =
        let val c = raisembox(`{#ROOT}`)
            val _ = send(r, (GET, self()))
            val x = rcv (`{}`, `{#ROOT}`, [ hn (GET, x) => x ])
            val _ = lowermbox(c, auth)
        in x end

    (** Set the value in `r` to its new value `x'`. *)
    fun set _ r x' = send(r, (SET, x'))

    (** Swap values in `r1` and `r2`. *)
    fun swap auth r1 r2 =
        let val x1 = get auth r1
            val x2 = get auth r2
            val _  = set r1 x2
            val _  = set r2 x1
        in () end

    (*--- Module ---*)
    (* TODO: Move the authority into "Ref_Make"? *)

    val Ref = {
        make    = make,
        destroy = destroy,
        get     = get,
        set     = set,
        swap    = swap
    }
in [("Ref", Ref)]
end

tests/lib/Ref.trp

import Ref

let val _ = print "-------------------------------------------"
    val _ = print "r = Ref.make authority 42@{}"
    val r = Ref.make authority 42
    val _ = printWithLabels (r)

    val _ = print "-------------------------------------------"
    val _ = print "Ref.get r"
    val _ = printWithLabels (Ref.get authority r)

    (* More tests, but those are not relevant here... *)
in () end

[ssoelvsten]

When doing the P2PCache i tried to use the rcv once more to send classified information looked up in the HashMap to the P2P layer of the runtime. I ended up with the following two errors:

Runtime error in thread d79a40cc-55f2-4252-b354-4da31cd73e71@{}%{}
>> Integrity level mismatch for lowering mailbox clearance
 | integrity level of the data: #root
 | integrity level of the target: #root-integrity

Runtime error in thread c1b0bb42-2aa0-441b-aaf2-e0ff7acaf8ac@{}%{}
>> Not enough mailbox clearance for this receive
 | receive lower bound: {}
 | receive upper bound: {#root}
 | pc level           : <#root-confidentiality;#root>
 | mailbox clearance  : {#ROOT}

Also kind of odd with the #root instead of #root-integrity.

But, it should be noted, this was fixable with a blockdecl prior to the send (and merely using a receive on the other end). Maybe the same applies to the above. If so, the problem might more be the error message.