Poly/ML RunCall结构相关技术问题咨询及实验现象解惑

背景 #

本人编程经验尚浅，在阅读Isabelle源码时接触到Poly/ML基础库的RunCall结构（例如在src/Pure/Concurrent/thread_attributes.ML中用于操作线程标志）。查阅Poly/ML基础库文档后未找到该结构的详细说明。在Intel Core i7环境的REPL中对RunCall.loadWord和RunCall.loadByte进行了实验，发现返回结果与预期不符，同时在Poly/ML 5.9+MacOS X Monterey+Intel Core i7环境中补充了实验，提出关于字节对象、字对象及地址追踪的假设，但仍需专业确认。

补充实验代码：

> 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. 何处可获取Poly/ML RunCall结构的详细手册或参考文档？ #

RunCall属于Poly/ML的内部底层接口，并未完全公开在官方基础库文档中，可通过以下途径获取信息：

• 查看Poly/ML的源码仓库，RunCall的实现和注释主要在runtime目录下的底层运行时代码中；
• 参考Isabelle的源码及相关技术文档，Isabelle大量使用RunCall做底层操作，部分代码注释会解释其用法；
• 参与Poly/ML或Isabelle的社区讨论（如邮件列表），核心开发者会针对这类底层接口给出解答；
• 查阅Poly/ML早期版本的文档或相关学术论文，部分内容可能对RunCall有更详细的说明。

2. 实验中RunCall.loadWord为何返回字符串的全部数据而非单个word？ #

这是因为你传入的参数是ref s（字符串的引用）而非字符串本身。在Poly/ML的内存布局中，ref引用对象的结构包含指向实际数据的指针，RunCall.loadWord会直接读取该引用对象起始地址的一个64位机器字（对应你的Intel i7环境）。返回值0wx3332310000000000000003其实包含了字符串的长度（低几位的0x3）和部分字符数据（0x31是'1'、0x32是'2'、0x33是'3'）——这是Poly/ML字符串对象的底层存储格式导致的：字符串对象头部会存储长度信息，后续才是实际字符数据。

如果直接传入字符串s而非ref s，RunCall.loadWord(s, 0w0)会读取字符串对象起始位置的机器字，也就是长度信息，而非全部字符数据。

3. 为何RunCall.loadWord与RunCall.loadByte的返回值差异巨大？ #

两者的核心差异在于读取单位和目标对象不同：

• RunCall.loadByte以字节为单位读取目标对象指定偏移处的数据。你传入的是字符串s，偏移0w0读取的是字符串对象头部的长度字节（0x3，对应字符串长度3）；由于64位环境下对象头部占8字节，偏移0w8开始才是实际字符数据，所以0w8对应'1'（0x31）、0w9对应'2'（0x32）、0w10对应'3'（0x33）；
• RunCall.loadWord以64位机器字为单位读取，你传入的是ref s，读取的是引用对象的整个机器字，包含指向字符串的指针相关信息和字符串的部分数据，因此返回的是一个64位大数值，和loadByte的单字节读取结果自然差异巨大。

另外，RunCall的这类函数是直接操作内存的底层接口，行为依赖于Poly/ML的内存布局和目标机器架构（如64位/32位、字节序等），返回结果需要结合这些底层细节理解。

内容的提问来源于stack exchange，提问作者opus26