Armada makes sure that concrete levels are compilable. One of the ways it does this is by ensuring that each instruction accesses no more than one shared-memory location. However, the code to do this is too conservative, sometimes considering an instruction to access multiple shared-memory locations when it actually doesn't.
For instance, if m and n are shared-memory locations, then it's not appropriate to read both m and n in the same instruction. But it should be legal to read their addresses in the same instruction, like MethodCall(&m, &n). Nevertheless, this is currently flagged as an illegal multiple shared-memory access. In other words, expressions like &m, &n, &arr[3], and &((*p).f) are counted as shared-memory accesses even when they don't involve accesses to shared memory.
Another instance of overcounting is when a method call accesses shared memory during both the call and the assignment of return variables. Currently, the instruction m := MethodCall(n) is flagged as an illegal multiple shared-memory access. But it would be fine to allow this, since the call step is modeled as a separate step from the assignment-of-return-variables step.
LukeXuan
commented
3 years ago
Armada makes sure that concrete levels are compilable. One of the ways it does this is by ensuring that each instruction accesses no more than one shared-memory location. However, the code to do this is too conservative, sometimes considering an instruction to access multiple shared-memory locations when it actually doesn't.
For instance, if m and n are shared-memory locations, then it's not appropriate to read both m and n in the same instruction. But it should be legal to read their addresses in the same instruction, like MethodCall(&m, &n). Nevertheless, this is currently flagged as an illegal multiple shared-memory access. In other words, expressions like &m, &n, &arr[3], and &((*p).f) are counted as shared-memory accesses even when they don't involve accesses to shared memory.
Another instance of overcounting is when a method call accesses shared memory during both the call and the assignment of return variables. Currently, the instruction m := MethodCall(n) is flagged as an illegal multiple shared-memory access. But it would be fine to allow this, since the call step is modeled as a separate step from the assignment-of-return-variables step.