The Non-Linearity of Volatile in Java

Linear logic and related logics (such as separation logic and fractional permissions) have proven useful in verifying concurrent programs because they make it easy to reason about heap separation properties. However "Volatile" fields in Java are difficult to reason about in strictly linear fashion. Volatile is much more easily handled using non-linear concepts such as immutability and ownership.