microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

Fix Shared-memory access counting #29

Closed LukeXuan closed 3 years ago

LukeXuan commented 3 years ago

This pull request should fix issue #14. The new algorithm for counting shared-memory access can be summarized as follows,

  1. +1 whenever GetLValue in ResolveAsLValue
  2. +1 whenver GetRValue in ResolveAsRValue
  3. +1 whenver UnaryOp.Dereference in ResolveAsRValue
  4. Resolution of LValue caused by UnaryOp.AddressOf doesn't count as a memory reference. This is dealt after the recursion.

In addition, the shared-memory access counting for method call arguments are separate from the rest of the statement. The reasoning is that a method call is translated into two separate next routines for call and return.

ghost commented 3 years ago

CLA assistant check
All CLA requirements met.