{"action":"created","issue":{"url":"https://api.github.com/repos/kwf/StrictCheck/issues/2","repository_url":"https://api.github.com/repos/kwf/StrictCheck","labels_url":"https://api.github.com/repos/kwf/StrictCheck/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/kwf/StrictCheck/issues/2/comments","events_url":"https://api.github.com/repos/kwf/StrictCheck/issues/2/events","html_url":"https://github.com/kwf/StrictCheck/issues/2","id":365435216,"node_id":"MDU6SXNzdWUzNjU0MzUyMTY=","number":2,"title":"observe produces wrong results and is not referentially transparent with ghc-8.6.1 and -O1 or -O2","user":{"login":"janpath","id":1183945,"node_id":"MDQ6VXNlcjExODM5NDU=","avatar_url":"https://avatars3.githubusercontent.com/u/1183945?v=4","gravatar_id":"","url":"https://api.github.com/users/janpath","html_url":"https://github.com/janpath","followers_url":"https://api.github.com/users/janpath/followers","following_url":"https://api.github.com/users/janpath/following{/other_user}","gists_url":"https://api.github.com/users/janpath/gists{/gist_id}","starred_url":"https://api.github.com/users/janpath/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/janpath/subscriptions","organizations_url":"https://api.github.com/users/janpath/orgs","repos_url":"https://api.github.com/users/janpath/repos","events_url":"https://api.github.com/users/janpath/events{/privacy}","received_events_url":"https://api.github.com/users/janpath/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-10-01T12:20:15Z","updated_at":"2018-10-01T18:28:46Z","closed_at":null,"author_association":"NONE","body":"I was just reading your paper and when reading about `entangle` and `observe` I thought that there was a good chance, that memorization would cause `observe` to use the same entangled value twice, thus giving false results.\r\n\r\nIndeed I found the following program, where that seems to be the case:\r\n\r\n```haskell\r\n{-# LANGUAGE GADTs #-}\r\n\r\nimport Test.StrictCheck\r\nimport Data.Foldable (traverse_)\r\nimport Data.Bifunctor (bimap)\r\n\r\nmain :: IO ()\r\nmain =\r\n  (print . bimap prettyDemand (\\(x :* Nil) -> prettyDemand x)) `traverse_` [\r\n    observe (\\() -> ()) (\\() -> ()) (),\r\n    observe (\\() -> ()) (\\_  -> ()) ()\r\n  ]\r\n```\r\n\r\nI would expect the following output:\r\n```\r\n(\"()\",\"()\")\r\n(\"()\",\"_\")\r\n```\r\n\r\nThis matches the actual output for ghc versions 8.2.2 and 8.4.3 with any optimisation level as well as ghc-8.6.1 with `-O0`. However when compiling with ghc-8.6.1 and `-O1` or `-O2` the actual output is this:\r\n```\r\n(\"()\",\"()\")\r\n(\"()\",\"()\")\r\n```\r\n\r\nEven worse, when we change the order of the two `observe`-calls in the list we get this:\r\n```\r\n(\"()\",\"_\")\r\n(\"()\",\"_\")\r\n```\r\n\r\nI think the best way to fix this would be to change `entangle` to this safe (exportable) version:\r\n```haskell\r\nentangle :: a -> IO (a, IORef (Thunk a))\r\nentangle =   do\r\n    ref <- newIORef Thunk\r\n    return ( unsafePerformIO $ do\r\n               writeIORef ref (Eval a)\r\n               return a\r\n           , ref )\r\n```\r\nThis version of entangle should be referentially transparent and allows the user to observe the evaluation status of the entangled value at different points in time. Furthermore, and most importantly for this issue, leaving out the outer `unsafePerformIO` makes sure that two calls to `entangle` will create two different entangled values with two different `IORef`s, thus making bugs like this impossible. However this of cause would probably require a lot of code to be rewritten to accommodate for the new type and maybe there is a quick and dirty solution that somehow prevents memorization or even not exporting observe and making sure it is only used in safe ways."},"comment":{"url":"https://api.github.com/repos/kwf/StrictCheck/issues/comments/426013225","html_url":"https://github.com/kwf/StrictCheck/issues/2#issuecomment-426013225","issue_url":"https://api.github.com/repos/kwf/StrictCheck/issues/2","id":426013225,"node_id":"MDEyOklzc3VlQ29tbWVudDQyNjAxMzIyNQ==","user":{"login":"kwf","id":597089,"node_id":"MDQ6VXNlcjU5NzA4OQ==","avatar_url":"https://avatars1.githubusercontent.com/u/597089?v=4","gravatar_id":"","url":"https://api.github.com/users/kwf","html_url":"https://github.com/kwf","followers_url":"https://api.github.com/users/kwf/followers","following_url":"https://api.github.com/users/kwf/following{/other_user}","gists_url":"https://api.github.com/users/kwf/gists{/gist_id}","starred_url":"https://api.github.com/users/kwf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kwf/subscriptions","organizations_url":"https://api.github.com/users/kwf/orgs","repos_url":"https://api.github.com/users/kwf/repos","events_url":"https://api.github.com/users/kwf/events{/privacy}","received_events_url":"https://api.github.com/users/kwf/received_events","type":"User","site_admin":false},"created_at":"2018-10-01T18:28:46Z","updated_at":"2018-10-01T18:28:46Z","author_association":"OWNER","body":"Thank you very much for this error report! It seems like the CSE pass in GHC 8.6 has gotten more aggressive. You're certainly right that all the variants of `observe` ought to have been `NOINLINE`-ed, and doing this should fix the issue permanently. I'll get on that shortly.\r\n\r\nIn the meantime, here's a more minimal example (which I'll add to the test suite shortly) and some details:\r\n\r\n```haskell\r\nimport System.Exit\r\nimport Test.StrictCheck\r\n\r\nmain :: IO ()\r\nmain =\r\n  let strict = prettyDemand (snd (observe1 id (\\() -> ()) ())) in\r\n  let lazy   = prettyDemand (snd (observe1 id (\\_  -> ()) ())) in\r\n\r\n  if strict /= lazy\r\n  then return ()\r\n  else die \"observe1 is not referentially transparent\"\r\n```\r\n\r\nWhen we compile this with `-O0`, it returns without error. With `-O1`, it errors out, as you would expect. However, with `-O1 -fno-case`, it is once more successfully. Here's how to replicate this:\r\n\r\n```bash\r\n$ ghc -fforce-recomp -no-keep-hi-files -no-keep-o-files -O0 -ddump-simpl Main.hs -o Unoptimized > Unoptimized.core\r\n$ ghc -fforce-recomp -no-keep-hi-files -no-keep-o-files -O1 -ddump-simpl Main.hs -o Optimized > Optimized.core\r\n$ ghc -fforce-recomp -no-keep-hi-files -no-keep-o-files -O1 -fno-cse -ddump-simpl Main.hs -o NoCSE > NoCSE.core\r\n```\r\n\r\nLooking at the generated `Optimized.core`, we can see the issue: there is only *one* instance of `entangleShape` in the entire core file—there should be 4 (or none, if there was no optimization at all).\r\n\r\n`Optimized.core` (excerpt):\r\n```haskell\r\n...\r\nMain.main5 :: () -> ((), Demand ())\r\n[GblId,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,\r\n         WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]\r\nMain.main5\r\n  = Test.StrictCheck.Observe.Unsafe.entangleShape\r\n      @ () Test.StrictCheck.Shaped.$fShaped()\r\n...\r\n```\r\n\r\nWe then see this single value `Main.main5` get re-used in three places, which causes the exact issue you observed. Whereas, without CSE, we see four separate instances of `entangleShape`.\r\n\r\n**Summary**: Allowing `observe` to be inlined exposes `entangleShape` to CSE optimization, which can destroy referential transparency. Fix: add `{-# NOINLINE #-}` pragmas to all `observe`-family functions, and add regression tests to the test suite. I'm on it."}}
{"actor":{"display_login":"kwf"}}