Consistent string-to-ident mapping across compilation units

[alxest]

Currently, different compilation units can have different string-to-ident mappings.
This is problematic for the pilot project I am working on (adding inter-procedural optimization to CompCert).
I found that several people also had similar problem, had a discussion and proposed a solution for this issue, but couldn't find the conclusion. (maybe discussed offline?)
May I ask current status of this issue? (Is there an agreed conclusion? Is the implementation underway?)

Thanks a lot!

[jeremie-koenig]

Hi Youngju, I don't think there have been any further developments.

My latest commits to #222 tried to safely encapsulate my changes into a module, with the goal of making it safer and having a pluggable way to introduce an alternative implementation for VST users along the lines of what @andrew-appel was suggesting. IIRC the added level of indirection slowed CompCert a bit.

If you need to push this forward, you could review the discussion, try to understand the design space, and do some experiments of your own.

One difficulty is that there are many requirements to take into account: the performance of CompCert, the performance of VST, convenience, limiting changes to the existing code as much as possible, and how safe a solution is when it involves axioms implemented with ML code. I'm not completely sure how important each one of these are to each person with a stake in this.

[xavierleroy]

I spent some time researching and proving efficient dictionary data structures (finite maps from strings), with mixed success so far. Some structures are quite fast after extraction, but not so fast when executed within Coq (as VST does). I still think that the way to go is to use Coq strings for C global variables and functions.

[andrew-appel]

One thing I found in my experiments is that it's not only about how fast the dictionaries are for lookup/insert (in Coq): proofs that carry large (dictionary) structures from one point to another (even without much looking-up) can be very slow, so the size matters even independent of the time taken per operation.