RunCall structure of Poly/ML

71 views Asked by At

I'm reading Isabelle's source code while I'm not experienced with programming in general. I found the use of RunCall structure of the Poly/ML basis library (e.g. in src/Pure/Concurrent/thread_attributes.ML to manipulate thread flags). I consulted the documentation of Poly/ML basis library for RunCall, but there is no detailed information for this structure probably because it's clear for well-experienced programmers.

I tried an experiment with RunCall.loadWord and RunCall.loadByte in REPL (with Intel Core i7): First, I got

> val x = "123";
val x = "123": string
> RunCall.loadWord(ref x, 0w0): word;
val it = 0wx3332310000000000000003: word

So loadWord somehow reads the address given by ref x. However, it returns not only the first 2 byte (= 1 word?) 0wx3332 but whole of the data of x: string. But

> RunCall.loadByte(ref x, 0w0): word;
val it = 0wxC8: word

and I cannot extract 0wxC8 from 0wx3332310000000000000003. Similarly,

> val n = 1;
val n = 1: int
> RunCall.loadWord(ref n, 0w0): word;
val it = 0wx1: word
> RunCall.loadByte(ref n, 0w0): word;
val it = 0wx3: word

and always loadByte returns twice plus one of the result of loadWord. (In this experiment, I supposed that ref x is something like &x of C language.)

So my questions are:

  1. Where can I find a manual for RunCall of Poly/ML? (Or some document giving a hint for RunCall.)
  2. In the above example, why loadWord returns not only one byte data 0wx33 but 0wx3332310000000000000003?
  3. In the above example, why loadWord and loadByte returns so different values?

I apologize that my confusion is probably coming from my lack of the basic knowledge on the memory architecture...


Addendum (this is at least in my environment (Poly/ML 5.9 Release + MacOS X Monterey + Intel Core i7)): I got a "hypothetical" answer to Q.3 (though I read only some comments in the source of Poly/ML). The points are

A. There are "byte-object" and "word-object" in Poly/ML and the first bit is used as a flag to distinguish these two types of object. The flag 0 is for "byte-object" and the flag 1 is for "word-object". The difference of these objects is the offset: it's 1 byte for "byte-object" and it's 1 word (= 2 byte in my case?) for "word-object".

B. RunCall.loadWord, when applied to string ref, it tracks (really???) the referenced address. But RunCall.loadByte does not.

By A., the behavior of the experiment with 1: int is clear. By B., the exotic value 0wxC8 is just coming from the (first one byte of the) address of the first byte of "123", so it depends on the runtime environment. The appropriate experiment was with

> val s = "123";
val s = "123": string
> RunCall.loadWord(ref s,0w0): word;
val it = 0wx3332310000000000000003: word
> RunCall.loadByte(s, 0w0): word;
val it = 0wx3: word
> RunCall.loadByte(s, 0w8): word;
val it = 0wx31: word
> RunCall.loadByte(s, 0w9): word;
val it = 0wx32: word
> RunCall.loadByte(s, 0w10): word;
val it = 0wx33: word

1

There are 1 answers

2
David Matthews On

The RunCall structure contains various very low-level operations and it is only there to allow some libraries to be built on top. It is deliberately undocumented and can change between releases or could even be removed completely.