Documenting the (dynamic) linking rules for symbol versioning

[Torvald Riegel]

On Wed, 2017-04-19 at 17:07 +0200, Michael Kerrisk (man-pages) wrote:
> The documentation around symbol versioning as used by the glibc dynamic
> linker (DL) is currently rather weak, and I'd like to add some pieces to
> various man pages (ld.so(8), dlsym(3), and possibly others) to improve
> this situation. Before that though, I'd rather like to check my
> understanding of the rules.

I can't comment on the specific questions you have, but I'd suggest to
reach out to Stephen Kell and Peter Sewell, as they have worked on
rigorous specifications of linking:
http://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf

That's static linking of course, but perhaps they'd be interested to
extend that work (or perhaps are already looking at this).

Sewell et al. have worked on rigorous specifications of memory models in
the past (eg, for C++), and those are *really* useful in practice.