You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: