jstolarek / slicer

Companion code for paper "Imperative Functional Programs that Explain their Work", Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, ICFP 2017, Oxford, UK
http://dl.acm.org/citation.cfm?id=3110258
GNU General Public License v3.0
6 stars 0 forks source link

Possible bug: Store invariants broken? #63

Closed jstolarek closed 7 years ago

jstolarek commented 7 years ago

The implementation of the Store logic might have a bug introduced by implementation of arrays:

Store { 
  { refs :: M.IntMap Value
  , arrs :: M.IntMap Array,
  , refCount :: Int

(Field names added for clarity.) The intention of refCount is to track the number of allocated references. So the invariant should be M.Size refs = refCount. This is invalidated by storeCreateArr:

storeCreateArr :: Store -> Int -> Value -> (Store, StoreLabel)
storeCreateArr (Store refs arrs refCount) dim v =
    (Store refs (M.insert refCount (mkArray dim v) arrs) (refCount + 1),
     StoreLabel refCount)

So now the invariant is M.Size refs + M.size arrs = refCount and keys in refs and arrs are not consecutive integers.

I'm not sure if this causes any problems - needs deeper investigation.

jamescheney commented 7 years ago

I didn't see anywhere it was assumed that M.size refs == refCount.

jstolarek commented 7 years ago

Indeed, I think this is no longer needed in the current code. This was definitely required at some point in the past, but I think this invariant might have become obsolete when I refactored Store to be abstract outside of Core module. I definitely want to take a closer look at this later to make sure this is indeed correct.

jstolarek commented 7 years ago

This looks good.