On Mon, 6 Apr 2009, Rob Arthan wrote:

I am trying to understand what level of binary compatibility I can expect if I use Poly/ML to create an executable by exporting a function which calls PolyML.rootFunction to give the users a Poly/ML interactive session. The users will then update the Poly/ML state, save it and reload it in later sessions using the functions in PolyML.SaveState. They will also load state files prebuilt for them.

If I build the executable on system A and create some saved state files there, how like A does some other system B have to be for the executable and the saved state files to work on B? I am concerned both about the compatibility for the saved state files and for the shared object files libpolyml.so and libpolymain.so. I understand QinetiQ have no problems moving between systems with Intel hardware and recent-ish slackware and Fedora operating systems. Would the same files work on my Intel Mac?

While David can probably explain better the true details, I can tell how we do it for Isabelle.

* We have a portable shell script that invents platform identifiers for combinations of HW and OS, according to "known equivalences". See http://isabelle.in.tum.de/repos/isabelle/file/tip/lib/scripts/polyml-platfor...

* We precompile Poly/ML for these equivalence classes of platforms as hinted in the README part of http://isabelle.in.tum.de/polyml-5.2.1/ It is important to use a "typical" representative of each platform equivalence class, neither too old, nor too new (to escape DLL-hell).

* We never "install" Poly/ML in a fixed place, but have a startup script that modifies LD_LIBRARY_PATH such that all libpoly* component are found again (on Mac OS this is DYLD_LIBRARY_PATH). Thus everything can be kept within a single "Isabelle" distribution directory, although this is not mandatory.

* Images produced by PolyML.SaveState are decorated by the same platform identifier. Poly/ML appears to require exactly the same executable to reload such an image.

This homegrown variant of "fat binaries" works quite well across a broad range of platforms, e.g. see the 7 platforms available via http://isabelle.in.tum.de/download_x86-linux.html

Only in rare situations, some users with very old Linux installations ever had to compile themselves.

Makarius

Rob Arthan wrote:

I am trying to understand what level of binary compatibility I can expect if I use Poly/ML to create an executable by exporting a function which calls PolyML.rootFunction to give the users a Poly/ML interactive session. The users will then update the Poly/ML state, save it and reload it in later sessions using the functions in PolyML.SaveState. They will also load state files prebuilt for them.

If I build the executable on system A and create some saved state files there, how like A does some other system B have to be for the executable and the saved state files to work on B? I am concerned both about the compatibility for the saved state files and for the shared object files libpolyml.so and libpolymain.so. I understand QinetiQ have no problems moving between systems with Intel hardware and recent-ish slackware and Fedora operating systems. Would the same files work on my Intel Mac?

The basic rule is that you can load a state file only into the executable that created it. More precisely, you can reload a state file into an executable that uses the object file that was created by a particular call to PolyML.export. So, if you compile your program and export it using PolyML.export("foo", PolyML.rootFunction) to get "foo.o", link it to make "polyfoo" and then save a state "bar.save" you can certainly reload "bar.save" in "polyfoo". You can also relink "foo.o" with any compatible version of libpolyml and the resulting executable will still load "bar.save".

The issue is what constitutes a compatible version of libpolyml. It must have the same architecture (i.e. i386 rather than x86_64 or PPC). It must also have a compatible interface number. Often new versions of the Poly/ML run-time system will have a different interface between the compiled ML code and the run-time system and the interface numbers will change. The biggest problem, though, for compatibility between Intel Macs and, say, Linux is that Linux uses ELF for its object files while the Mac uses Macho. This means that you cannot take a "foo.o" built on Linux and link it on the Mac because the Mac linker will simply not recognise it. To get a "foo.o" on the Mac you would have to recompile your source and re-export but now you'd have a different "foo.o". This therefore means that it's not possible to build a binary on the Mac that will read a saved state produced on Linux. It might be possible to build a tool to convert the Linux object file to Macho. There may even be such a tool. Doing it for a Poly/ML export file would be much simpler than for a general object file.

The reason for the rule about only being able to load a saved state into the same object file is to guarantee that it's safe. A saved state does not contain any immutable data that is present in the executable. Instead it just uses a pointer to the data in the executable. To allow the system to load saved states and executables at different addresses the saved state contains relocation information but this simply says that the object is at a particular offset within a particular segment in the executable. If the saved state were loaded into an executable where that offset did not correspond to the start of the required object there would be complete chaos. The only way to guarantee this is to put a stamp into the executable, actually into the object file when it's created by PolyML.export, and store this in any saved state. When the state is loaded the stamps are compared and if they don't match the load fails. There is no way to guarantee that two different calls to PolyML.export will generate object files with the data laid out in exactly the same way. Even two successive calls to PolyML.export could produce slightly different object files due to re-ordering by the garbage collector.

On a related topic: I have had no success trying to link polyml statically. I I use -Wl,-Bstatic -lpolymain -lpolyml -Wl,-Bdynamic on the command line, I get screeds of undefined reference messages. Is static linking an option to build a binary that can be run without installing Poly/ML? If so, how do I do it?

I'm not certain of this but I think you need to give the right options to configure to make sure it's building static libraries. I've just tested building Poly/ML with ./configure --disable-shared && make and it appears to make a statically linked version of "poly". Poly/ML uses libtool to do all this so check the documentation for that.

David.