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:
- Where can I find a manual for
RunCall
of Poly/ML? (Or some document giving a hint forRunCall
.) - In the above example, why
loadWord
returns not only one byte data0wx33
but0wx3332310000000000000003
? - In the above example, why
loadWord
andloadByte
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
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.