Distributing read permissions between threads

[pieter-bos]

(author: @bobismijnnaam)

A possible use case of read permissions is to distribute read permission between threads:

par (int tid = 0 .. N)
requires x != null ** Perm(x.f, read);
{
  m1(x.f)
} and 
requires x != null ** Perm(x.f, read);
{
  m2(x.f);
}

This results in the following quantifier for the parallel region:

(\forall int tid = 0 .. N; Perm(x.f, read))

However, because of viper's injectivity requirement, this expression is not well-formed.

The following rewrite rules can be used to resolve this:

axiom read_spreads_l {
  Perm(g1, read * i)
  ==
  i > 0 ==> Perm(g1, read)
}

axiom read_spreads_r {
  Perm(g1, i * read)
  ==
  i > 0 ==> Perm(g1, read)
}

axiom resource_independent_read_quant {
  (\forall* int tid; (tid \memberof {(e1!tid)..(e2!tid)}); (Perm(g1, read)!tid))
  ==
  (e1<e2) ==> Perm(g1, read)
}

Unfortunately, these rules cause some problems. Besides sidestepping this injectivity requirement, using these rewrite rules does not accurately reflect Viper's intended semantics of read (see: viperproject/silicon#539). Furthermore, at the time of writing this it is also not allowed to have complex expressions composed of `read (see: viperproject/silicon#569), which would be needed to use more complicated alternative rewrite rules (see below).

Currently, the only way of working around this is by using the fact that the number of threads is usually known (in the above example, the number of threads is N). This allows permissions to be distributed in portions of 1\N. A downside of this is that when the expressions become more complicated (say, when you have N producers, and one consumer, portions are of size 1\(N+1)), Viper/Z3 can sometimes not deal with the resulting non-linear arithmetic, which can cause long verification times and non-determinism.

Alternative formulations of the rewrite rules

Briefly the following alternative formulation was used in vercors:

axiom read_spreads_l {
  read * i
  ==
  (\let int canary = i; i == 0 ? read : read)
}

axiom read_spreads_r {
  i * read
  ==
  (\let int canary = i; i == 0 ? read : read)
}

These leave the value i outside of the multiplication, but do keep i around because it needs to be well-formed. For example, if i were 1/0, removing it would be unsound. However, these rules are currently not allowed because of viperproject/silicon#569.