Comments on: Introducing Speculation http://comonad.com/reader/2010/introducing-speculation/ types, (co)monads, substructural logic Sat, 29 Dec 2012 15:18:06 -0800 http://wordpress.org/?v=2.8.4 hourly 1 By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-30881 Edward Kmett Sun, 26 Dec 2010 20:45:05 +0000 http://comonad.com/reader/?p=205#comment-30881 @Rafael: Good idea =) @Rafael: Good idea =)

]]>
By: Rafael Calsaverini http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-30823 Rafael Calsaverini Sun, 26 Dec 2010 03:22:04 +0000 http://comonad.com/reader/?p=205#comment-30823 This may be useful for Markov Chain Monte Carlo simulations by using the guess that the new sample proposal will be rejected... seems interesting. This may be useful for Markov Chain Monte Carlo simulations by using the guess that the new sample proposal will be rejected… seems interesting.

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-21221 Edward Kmett Wed, 22 Sep 2010 20:28:00 +0000 http://comonad.com/reader/?p=205#comment-21221 Apparently, undefined will sometimes claim to be evaluated. Now I need to chase bottoms too! Apparently, undefined will sometimes claim to be evaluated. Now I need to chase bottoms too!

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-20828 Edward Kmett Thu, 16 Sep 2010 11:11:52 +0000 http://comonad.com/reader/?p=205#comment-20828 FYI, I did wind up adding that info table check to the tag-bits library, although I do so only after checking the tag bits themselves as a fallback. It works well, and lets the library be useful even from ghci. Thanks! FYI, I did wind up adding that info table check to the tag-bits library, although I do so only after checking the tag bits themselves as a fallback.

It works well, and lets the library be useful even from ghci.

Thanks!

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18805 Edward Kmett Mon, 02 Aug 2010 15:30:02 +0000 http://comonad.com/reader/?p=205#comment-18805 That said, it might be worthwhile to add that as a second check, assuming we can get something like the unboxed version to work in the first place. That way it could check the tag bits, and if zero, before giving up it could double check the info table, that way we avoid having to actually use the target object in case where the tag bits having been propagated, which potentially avoids paging it in. That said, it might be worthwhile to add that as a second check, assuming we can get something like the unboxed version to work in the first place.

That way it could check the tag bits, and if zero, before giving up it could double check the info table, that way we avoid having to actually use the target object in case where the tag bits having been propagated, which potentially avoids paging it in.

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18804 Edward Kmett Mon, 02 Aug 2010 15:26:00 +0000 http://comonad.com/reader/?p=205#comment-18804 I was deliberately avoiding reading the info table to avoid dealing with variations in ghc compilation options changing the layout. I'll revert to the boxed version for now I guess and then see if I can get a better way to do the unsafeCoerce# without forcing. I was deliberately avoiding reading the info table to avoid dealing with variations in ghc compilation options changing the layout.

I’ll revert to the boxed version for now I guess and then see if I can get a better way to do the unsafeCoerce# without forcing.

]]>
By: pepeiborra http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18803 pepeiborra Mon, 02 Aug 2010 15:03:58 +0000 http://comonad.com/reader/?p=205#comment-18803 Ed, thanks for the tips. I tried inserting a call to performGC in the example, but it didn't help the boxed version. main = do let i = trace "--> evaluated" () putStrLn $ "tagbits: " ++ show (unsafeGetTagBits i) print i performGC >> putStrLn "--> GC performed" putStrLn $ "tagbits: " ++ show (unsafeGetTagBits i) pepe:~/Dropbox/code/snippets$ ghc --make TagBits&& ./TagBits Linking TagBits ... tagbits: 0 --> evaluated () --> GC performed tagbits: 0 Nevertheless, I have gone back to my actual use case (pruning the non-evaluated branches of an incomplete infinite proof tree, for display purposes), and found I was traversing the tree bottom-up, with a non strict fold. In a bottom-up traversal, the boxed version was *correctly* returning False for subtrees (since the fold is lazy), whereas the unboxed version was actually seq'ing subtrees and returning True, which in the particular example at hand was what I expected. Hence the unboxed version was hiding an actual mistake in my reasoning. Now the boxed version works as expected with a top-down traversal. To see why the unboxed version forces evaluation of the argument, let's look at the core generated by ghc: Data.TagBits.unsafeGetTagBits = \ (@ a_aqz) (a_syV :: a_aqz) -> case a_syV `cast` (CoUnsafe a_aqz GHC.Prim.Word# :: a_aqz ~ GHC.Prim.Word#) of wild_syX { __DEFAULT -> case GHC.Prim.and# wild_syX __word 3 of sat_sz3 { __DEFAULT -> GHC.Word.W# sat_sz3 } } There is a case expression where the scrutinee is the argument. Unless I am wrong, this case expression forces the evaluation of the argument. If you are curious I also cooked a version of unsafeIsEvaluated which avoids the tricky pointer tagging business and looks directly at the info table: http://gist.github.com/504764 Ed,

thanks for the tips. I tried inserting a call to performGC in the example, but it didn’t help the boxed version.

main = do
let i = trace “–> evaluated” ()
putStrLn $ “tagbits: ” ++ show (unsafeGetTagBits i)
print i
performGC >> putStrLn “–> GC performed”
putStrLn $ “tagbits: ” ++ show (unsafeGetTagBits i)

pepe:~/Dropbox/code/snippets$ ghc –make TagBits&& ./TagBits
Linking TagBits …
tagbits: 0
–> evaluated
()
–> GC performed
tagbits: 0

Nevertheless, I have gone back to my actual use case (pruning the non-evaluated branches of an incomplete infinite proof tree, for display purposes), and found I was traversing the tree bottom-up, with a non strict fold. In a bottom-up traversal, the boxed version was *correctly* returning False for subtrees (since the fold is lazy), whereas the unboxed version was actually seq’ing subtrees and returning True, which in the particular example at hand was what I expected. Hence the unboxed version was hiding an actual mistake in my reasoning. Now the boxed version works as expected with a top-down traversal.

To see why the unboxed version forces evaluation of the argument, let’s look at the core generated by ghc:

Data.TagBits.unsafeGetTagBits =
\ (@ a_aqz) (a_syV :: a_aqz) ->
case a_syV
`cast` (CoUnsafe a_aqz GHC.Prim.Word# :: a_aqz ~ GHC.Prim.Word#)
of wild_syX { __DEFAULT ->
case GHC.Prim.and# wild_syX __word 3 of sat_sz3 { __DEFAULT ->
GHC.Word.W# sat_sz3
}
}

There is a case expression where the scrutinee is the argument. Unless I am wrong, this case expression forces the evaluation of the argument.

If you are curious I also cooked a version of unsafeIsEvaluated which avoids the tricky pointer tagging business and looks directly at the info table: http://gist.github.com/504764

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18776 Edward Kmett Sun, 01 Aug 2010 18:39:10 +0000 http://comonad.com/reader/?p=205#comment-18776 @Pepe: There are a couple of things happening here. You definitely shouldn't be getting segfaults on the unboxed version. If so, then I have faulty reasoning and will need to revert to the boxed version. With regards to the boxed version still showing unevaluated-ness, what you're experiencing is that the 'i' value at that point still points to the indirection because a garbage collection hasn't happened yet to propagate the tag bits. I'd hazard that if you inserted a call to performGc in the middle there that you'd start seeing the tags. @Pepe: There are a couple of things happening here.

You definitely shouldn’t be getting segfaults on the unboxed version. If so, then I have faulty reasoning and will need to revert to the boxed version.

With regards to the boxed version still showing unevaluated-ness, what you’re experiencing is that the ‘i’ value at that point still points to the indirection because a garbage collection hasn’t happened yet to propagate the tag bits. I’d hazard that if you inserted a call to performGc in the middle there that you’d start seeing the tags.

]]>
By: pepeiborra http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18767 pepeiborra Sun, 01 Aug 2010 11:37:34 +0000 http://comonad.com/reader/?p=205#comment-18767 Looking at the unboxed version of unsafeGetTagBits, defined as: unsafeGetTagBits a = W# (and# (unsafeCoerce# a) (int2Word# mask#)) I believe that this performs some evaluation of its argument. The program import Data.TagBits import Debug.Trace main = do let i = trace "X" [1] print (unsafeGetTagBits i) print i print (unsafeGetTagBits i) produces the output X 2 [1] 2 Also, I have been experiencing segfaults with this unboxed version. The boxed version does not segfault nor perform any evaluation, but in my experiments it seems to return always the value 0. For the program above, I obtain 0 X [1] 0 Concretely, I am using this code: data Box a = Box a unsafeGetTagBits a = unsafeCoerce (Box a) .&. fromIntegral (sizeOf (undefined :: Int) - 1) Any idea of what is going on? Looking at the unboxed version of unsafeGetTagBits, defined as:

unsafeGetTagBits a = W# (and# (unsafeCoerce# a) (int2Word# mask#))

I believe that this performs some evaluation of its argument. The program

import Data.TagBits
import Debug.Trace

main = do
let i = trace “X” [1]
print (unsafeGetTagBits i)
print i
print (unsafeGetTagBits i)

produces the output

X
2
[1]
2

Also, I have been experiencing segfaults with this unboxed version.

The boxed version does not segfault nor perform any evaluation, but in my experiments it seems to return always the value 0.
For the program above, I obtain

0
X
[1]
0

Concretely, I am using this code:

data Box a = Box a
unsafeGetTagBits a = unsafeCoerce (Box a) .&. fromIntegral (sizeOf (undefined :: Int) – 1)

Any idea of what is going on?

]]>
By: Edward Kmett http://comonad.com/reader/2010/introducing-speculation/comment-page-1/#comment-18645 Edward Kmett Wed, 28 Jul 2010 13:34:03 +0000 http://comonad.com/reader/?p=205#comment-18645 @Asger: You could likely exploit the speculation primitive if you supply your own equality check that checked fitness instead of value and used it to wrap the continuation, but I'll admit I haven't thought it through in depth. @Asger: You could likely exploit the speculation primitive if you supply your own equality check that checked fitness instead of value and used it to wrap the continuation, but I’ll admit I haven’t thought it through in depth.

]]>