1
Vote

generalizing _(by_claim)

description

Currently, _(by_claim c, e) can be used only to read nonvolatile fields. We should be able to use it to also read volatile fields; indeed, we should be able to use it to read through an arbitrary pointer. The translation would just be

_(assert \forall \state s1,s2; \at(s1,\active_claim(c) && \full_stop()) && \at(s2,\active_claim(c) && \full_stop()) ==> \at(s1,e) == \at(s2,e))

comments

erniecohen wrote Aug 5, 2012 at 2:35 PM

Even more importantly, _(by_claim) shouldn't be restricted to claims; it should just use ordinary closed object lists (lists like _(atomic), except that all of the items on the list are implicitly _(read_only). We should also rename it something like _(sequential_read).

Sign in to add a comment or to set email notifications