New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Surprising behavior of weak hashtables and hash-consing #6941
Comments
Comment author: @gasche (1) Which OCaml version are you using? |
Comment author: bvaugon It looks like a memory corruption. Since (Printf.fprintf "0") and If you are in 4.02.0 or later, the OCaml implementation of Printf no To debug that and track memory corruptions, a basic way is to |
Comment author: disteph Ah, got it. I tested with 4.02.2 and 4.02.3, same thing. Is the Weak module using unsafe things like Obj? I did not know. I'm not sure how I can track it down, though. My code barely use the Weak functions. |
Comment author: disteph I've attached my code. |
Comment author: bvaugon That's strange. The Weak modules is (a priori) safe and can't break |
Comment author: disteph It is part of the program that has the strange behaviour. The rest of my code was organised under the assumption that if one attempts to construct the same term twice, then the second time, the term is found in the hash-consing table and a pointer to the first construct is returned, with the same id and the property that you can check the equality with the pointers or with the ids. But obviously the assumption is not true with a hash-consing table built with Weak, since the gc can remove the entry between the first time and the second time the term is built. If that happens, the id of the term at the second construction is different from the id of the same term, now erased, at the first construction. And when my code then checked whether the term, arising from the second construction, belongs to a set (implemented as a Patricia trie), the first id was in there but not the second, so the answer was incorrectly negative. And whether the garbage collector erased the term between its first construction and the second construction was obviously sensitive to a lot of irrelevant things, such as how many Format.fprintf I had done or whether I was compiling native code or byte code. My bad. I should have know better. Sorry for having wasted your time... |
Comment author: @xavierleroy I'm taking the liberty to mark this PR as resolved. I also updated the summary. There are ways to implement reliable hash-consing using weak hash tables, see http://moscova.inria.fr/~doligez/publications/cuoq-doligez-mlw-2008.pdf If you still observe weird behaviors in an implementation of hash-consing similar to that of Cuoq and Doligez, please reopen this PR. |
Original bug ID: 6941
Reporter: disteph
Status: closed (set by @xavierleroy on 2017-02-16T14:16:41Z)
Resolution: not a bug
Priority: normal
Severity: minor
Platform: Linux
OS: Ubuntu
OS Version: Ubuntu 14.04
Version: 4.02.3
Category: ~DO NOT USE (was: OCaml general)
Monitored by: @yakobowski
Bug description
Wrote a 5000 line SAT-solver in OCaml, some answers are wrong.
While debugging, I tweaked the print_in_fmt function that I wrote to pretty-print literals (basically, these are strings)
Changing the line
Format.fprintf fmt "0"
to
Format.fprintf fmt ""
changes the output of my SAT-solver from SAT to UNSAT (the latter being the correct answer).
I don't know how Format.fprintf is implemented and compiled, it must have some important side-effect that apparently affects the rest of my (otherwise purely functional) code.
Moreover, I get different answers if I compile in native (my problem is erroneously diagnosed as SAT) or in bytecode (my problem is correctly diagnosed as UNSAT), but the source code is the same.
I know this is probably a debugging issue of my own code, and I'm trying to investigate how a side-effect of Format.fprintf could affect the rest of my code, but with different behaviours given in native and bytecode, any hint is appreciated.
Steps to reproduce
I can try to reduce my code to something minimal, but as it will take me a lot of time, any idea is appreciated is appreciated about the different behaviours of Format.fprintf in native or bytecode.
File attachments
The text was updated successfully, but these errors were encountered: