From 5d3f8e64632a5e7be96ac7882529d2e4d6f23e78 Mon Sep 17 00:00:00 2001
From: mbaxter
+
+
+
Overview
single instruction encoded in the state to produce a new state .
Thus, the trace of a program executed by the FPVM is an ordered set of VM states.
+Boolean
- An 8-bit boolean value equal to 0 (false) or 1 (true).Byte
- An 8-bit value.Hash
- A 256-bit fixed-size value produced by the Keccak-256 cryptographic hash function.UInt64
- A 64-bit unsigned integer value.Word
- A 32-bit value.MaxWord
- A Word
with all bits set to 1: 0xFFFFFFFF
.
+When interpreted as a signed value, this is equivalent to -1.WordSize
- The number of bytes in a Word
(4).MTCannon adds support for multithreading. @@ -352,7 +373,7 @@
Wakeup traversal is completed by setting the FPVM state's wakeup
field to 0xFFFFFFFF
(-1),
+
Wakeup traversal is completed by setting the FPVM state's wakeup
field to MaxWord
,
causing the FPVM to resume normal execution.
Threads enter a waiting state when a futex wait syscall is successfully executed, setting the thread's
futexAddr
, futexVal
, and futexTimeoutStep
fields according to the futex syscall arguments.
During normal execution, when the active thread is in a waiting state (its futexAddr
is not 0xFFFFFFFF
), the VM
+
During normal execution, when the active thread is in a waiting state (its futexAddr
is not equal to MaxWord
), the VM
checks if it can be woken up.
A waiting thread will be woken up if:
The VM will wake such a thread by resetting its futex fields:
futexAddr
= 0xFFFFFFFF
futexAddr
= MaxWord
futexVal
= 0futexTimeoutStep
= 0The FPVM is a state transition function that operates on a state object consisting of the following fields:
memRoot
- A bytes32
value representing the merkle root of VM memory.preimageKey
- bytes32
value of the last requested pre-image key.preimageOffset
- The 32-bit value of the last requested pre-image offset.heap
- 32-bit base address of the most recent memory allocation via mmap.llReservationActive
- 8-bit boolean indicator of whether a memory reservation,
+memRoot
- [Hash
] A value representing the merkle root of VM memory.preimageKey
- [Hash
] The value of the last requested pre-image key.preimageOffset
- [Word
] The value of the last requested pre-image offset.heap
- [Word
] The base address of the most recent memory allocation via mmap.llReservationActive
- [Boolean
] Indicates whether a memory reservation,
which is reserved via a Load Linked Word (ll
) instruction, is active.llAddress
- 32-bit address of the currently active memory reservation if one exists.llOwnerThread
- 32-bit id of the thread that initiated the current memory reservation if one exists.exitCode
- 8-bit exit code.exited
- 8-bit boolean valuel indicating whether the VM has exited.step
- 64-bit step counter.stepsSinceLastContextSwitch
- 64-bit step counter that tracks the number of steps executed on the current
+llAddress
- [Word
] The address of the currently active memory reservation if one exists.llOwnerThread
- [Word
] The id of the thread that initiated the current memory reservation if one exists.exitCode
- [Byte
] The exit code value.exited
- [Boolean
] Indicates whether the VM has exited.step
- [UInt64
] A step counter.stepsSinceLastContextSwitch
- [UInt64
] A step counter that tracks the number of steps executed on the current
thread since the last preemption.wakeup
- 32-bit address set via a futex syscall signaling that the VM has entered wakeup traversal or else
-0xFFFFFFFF
(-1) if there is no active wakeup signal. For details see "Wakeup Traversal".traverseRight
- 8-bit boolean that indicates whether the currently active thread is on the left or right thread
+wakeup
- [Word
] The address set via a futex syscall signaling that the VM has entered wakeup traversal or else
+MaxWord
if there is no active wakeup signal. For details see "Wakeup Traversal".traverseRight
- [Boolean
] Indicates whether the currently active thread is on the left or right thread
stack, as well as some details on thread traversal mechanics.
See "Thread Traversal Mechanics" for details.leftThreadStack
- a bytes32
hash of the contents of the left thread stack.
+leftThreadStack
- [Hash
] A hash of the contents of the left thread stack.
For details, see the “Thread Stack Hashing” section.rightThreadStack
- a bytes32
hash of the contents of the right thread stack.
+rightThreadStack
- [Hash
] A hash of the contents of the right thread stack.
For details, see the “Thread Stack Hashing” section.nextThreadID
- 32-bit value defining the id to assign to the next thread that is created.nextThreadID
- [Word
] The value defining the id to assign to the next thread that is created.The state is represented by packing the above fields, in order, into a 172-byte buffer.
The state of a single thread is tracked and represented by a thread state object consisting of the following fields:
threadID
- 32-bit unique thread identifier.exitCode
- 8-bit exit code.exited
- 8-bit boolean value indicating whether the thread has exited.futexAddr
- 32-bit address set via a futex syscall indicating that this thread is waiting on a value change
+threadID
- [Word
] A unique thread identifier.exitCode
- [Byte
] The exit code value.exited
- [Boolean
] Indicates whether the thread has exited.futexAddr
- [Word
] An address set via a futex syscall indicating that this thread is waiting on a value change
at this address.futexVal
- 32-bit value representing the memory contents at futexAddr
when this thread began waiting.futexTimeoutStep
- 64-bit value representing the future step
at which the futex wait will time out. Set to the
-max uint64 value (-1) if no timeout is active.pc
- 32-bit program counter.nextPC
- 32-bit next program counter. Note that this value may not always be
+futexVal
- [Word
] A value representing the memory contents at futexAddr
when this thread began waiting.futexTimeoutStep
- [UInt64
] A value representing the future step
at which the futex wait will time out.
+Set to MaxWord
if no timeout is active.pc
- [Word
] The program counter.nextPC
- [Word
] The next program counter. Note that this value may not always be
when executing a branch/jump delay slot.lo
- 32-bit MIPS LO special register.hi
- 32-bit MIPS HI special register.registers
- General-purpose MIPS32 registers. Each register is a 32-bit value.lo
- [Word
] The MIPS LO special register.hi
- [Word
] The MIPS HI special register.registers
- 32 general-purpose MIPS registers numbered 0 - 31. Each register contains a Word
value.A thread is represented by packing the above fields, in order, into a 166-byte buffer.
memRoot
represents the merkle root of the tree, reflecting the effects of memory writes.
-As a result of this memory representation, all memory operations are 4-byte aligned.
+As a result of this memory representation, all memory operations are WordSize
-byte aligned.
Memory access doesn't require any privileges. An instruction step can access any memory
location as the entire address space is unprotected.
For all of the following syscalls, an error is indicated by setting the return
-register ($v0
) to 0xFFFFFFFF
(-1) and errno
($a3
) is set accordingly.
+register ($v0
) to MaxWord
and errno
($a3
) is set accordingly.
The VM must not modify any register other than $v0
and $a3
during syscall handling.
The following tables summarize supported syscalls and their behaviors. If an unsupported syscall is encountered, the VM will raise an exception.
@@ -582,7 +603,7 @@futex_op
's FUTEX_WAIT_PRIVATE
(128) and FUTEX_WAKE_PRIVATE
(129). Other operations set errno to 0x16
.0x9
.clock_id
's REALTIME
(0) and MONOTONIC
(1). For other clock_id
's, sets errno to 0x16
. Calculates a deterministic time value based on the state's step
field and a constant HZ
(10,000,000) where HZ
represents the approximate clock rate (steps / second) of the FPVM:seconds = step/HZ
nsecs = (step % HZ) * 10^9/HZ
addr
and nsecs are set at addr + 4
.clock_id
's REALTIME
(0) and MONOTONIC
(1). For other clock_id
's, sets errno to 0x16
. Calculates a deterministic time value based on the state's step
field and a constant HZ
(10,000,000) where HZ
represents the approximate clock rate (steps / second) of the FPVM:seconds = step/HZ
nsecs = (step % HZ) * 10^9/HZ
addr
and nsecs are set at addr + WordSize
.Syscalls referencing unknown file descriptors fail with an EBADF
errno as done on Linux.
Writing to and reading from standard output, input and error streams have no effect on the FPVM state. FPVM implementations may use them for debugging purposes as long as I/O is stateless.
-All I/O operations are restricted to a maximum of 4 bytes per operation. -Any read or write syscall request exceeding this limit will be truncated to 4 bytes. -Consequently, the return value of read/write syscalls is at most 4, indicating the actual number of bytes read/written.
+All I/O operations are restricted to a maximum of WordSize
bytes per operation.
+Any read or write syscall request exceeding this limit will be truncated to WordSize
bytes.
+Consequently, the return value of read/write syscalls is at most WordSize
bytes,
+indicating the actual number of bytes read/written.
Writing to stderr/stdout standard stream always succeeds with the write count input returned, effectively continuing execution without writing work. @@ -656,11 +680,11 @@
As mentioned earlier in memory, all memory operations are 4-byte aligned. +
As mentioned earlier in memory, all memory operations are WordSize
-byte aligned.
Since pre-image I/O occurs on memory, all pre-image I/O operations must strictly adhere to alignment boundaries.
This means the start and end of a read/write operation must fall within the same alignment boundary.
If an operation were to violate this, the input count
of the read/write syscall must be
@@ -679,7 +703,6 @@
Thus, the trace of a program executed by the FPVM is an ordered set of VM states.
+Boolean
- An 8-bit boolean value equal to 0 (false) or 1 (true).Byte
- An 8-bit value.Hash
- A 256-bit fixed-size value produced by the Keccak-256 cryptographic hash function.UInt64
- A 64-bit unsigned integer value.Word
- A 32-bit value.MaxWord
- A Word
with all bits set to 1: 0xFFFFFFFF
.
+When interpreted as a signed value, this is equivalent to -1.WordSize
- The number of bytes in a Word
(4).MTCannon adds support for multithreading. @@ -12701,7 +12722,7 @@
Wakeup traversal is completed by setting the FPVM state's wakeup
field to 0xFFFFFFFF
(-1),
+
Wakeup traversal is completed by setting the FPVM state's wakeup
field to MaxWord
,
causing the FPVM to resume normal execution.
Threads enter a waiting state when a futex wait syscall is successfully executed, setting the thread's
futexAddr
, futexVal
, and futexTimeoutStep
fields according to the futex syscall arguments.
During normal execution, when the active thread is in a waiting state (its futexAddr
is not 0xFFFFFFFF
), the VM
+
During normal execution, when the active thread is in a waiting state (its futexAddr
is not equal to MaxWord
), the VM
checks if it can be woken up.
A waiting thread will be woken up if:
The VM will wake such a thread by resetting its futex fields:
futexAddr
= 0xFFFFFFFF
futexAddr
= MaxWord
futexVal
= 0futexTimeoutStep
= 0The FPVM is a state transition function that operates on a state object consisting of the following fields:
memRoot
- A bytes32
value representing the merkle root of VM memory.preimageKey
- bytes32
value of the last requested pre-image key.preimageOffset
- The 32-bit value of the last requested pre-image offset.heap
- 32-bit base address of the most recent memory allocation via mmap.llReservationActive
- 8-bit boolean indicator of whether a memory reservation,
+memRoot
- [Hash
] A value representing the merkle root of VM memory.preimageKey
- [Hash
] The value of the last requested pre-image key.preimageOffset
- [Word
] The value of the last requested pre-image offset.heap
- [Word
] The base address of the most recent memory allocation via mmap.llReservationActive
- [Boolean
] Indicates whether a memory reservation,
which is reserved via a Load Linked Word (ll
) instruction, is active.llAddress
- 32-bit address of the currently active memory reservation if one exists.llOwnerThread
- 32-bit id of the thread that initiated the current memory reservation if one exists.exitCode
- 8-bit exit code.exited
- 8-bit boolean valuel indicating whether the VM has exited.step
- 64-bit step counter.stepsSinceLastContextSwitch
- 64-bit step counter that tracks the number of steps executed on the current
+llAddress
- [Word
] The address of the currently active memory reservation if one exists.llOwnerThread
- [Word
] The id of the thread that initiated the current memory reservation if one exists.exitCode
- [Byte
] The exit code value.exited
- [Boolean
] Indicates whether the VM has exited.step
- [UInt64
] A step counter.stepsSinceLastContextSwitch
- [UInt64
] A step counter that tracks the number of steps executed on the current
thread since the last preemption.wakeup
- 32-bit address set via a futex syscall signaling that the VM has entered wakeup traversal or else
-0xFFFFFFFF
(-1) if there is no active wakeup signal. For details see "Wakeup Traversal".traverseRight
- 8-bit boolean that indicates whether the currently active thread is on the left or right thread
+wakeup
- [Word
] The address set via a futex syscall signaling that the VM has entered wakeup traversal or else
+MaxWord
if there is no active wakeup signal. For details see "Wakeup Traversal".traverseRight
- [Boolean
] Indicates whether the currently active thread is on the left or right thread
stack, as well as some details on thread traversal mechanics.
See "Thread Traversal Mechanics" for details.leftThreadStack
- a bytes32
hash of the contents of the left thread stack.
+leftThreadStack
- [Hash
] A hash of the contents of the left thread stack.
For details, see the “Thread Stack Hashing” section.rightThreadStack
- a bytes32
hash of the contents of the right thread stack.
+rightThreadStack
- [Hash
] A hash of the contents of the right thread stack.
For details, see the “Thread Stack Hashing” section.nextThreadID
- 32-bit value defining the id to assign to the next thread that is created.nextThreadID
- [Word
] The value defining the id to assign to the next thread that is created.The state is represented by packing the above fields, in order, into a 172-byte buffer.
The state of a single thread is tracked and represented by a thread state object consisting of the following fields:
threadID
- 32-bit unique thread identifier.exitCode
- 8-bit exit code.exited
- 8-bit boolean value indicating whether the thread has exited.futexAddr
- 32-bit address set via a futex syscall indicating that this thread is waiting on a value change
+threadID
- [Word
] A unique thread identifier.exitCode
- [Byte
] The exit code value.exited
- [Boolean
] Indicates whether the thread has exited.futexAddr
- [Word
] An address set via a futex syscall indicating that this thread is waiting on a value change
at this address.futexVal
- 32-bit value representing the memory contents at futexAddr
when this thread began waiting.futexTimeoutStep
- 64-bit value representing the future step
at which the futex wait will time out. Set to the
-max uint64 value (-1) if no timeout is active.pc
- 32-bit program counter.nextPC
- 32-bit next program counter. Note that this value may not always be
+futexVal
- [Word
] A value representing the memory contents at futexAddr
when this thread began waiting.futexTimeoutStep
- [UInt64
] A value representing the future step
at which the futex wait will time out.
+Set to MaxWord
if no timeout is active.pc
- [Word
] The program counter.nextPC
- [Word
] The next program counter. Note that this value may not always be
when executing a branch/jump delay slot.lo
- 32-bit MIPS LO special register.hi
- 32-bit MIPS HI special register.registers
- General-purpose MIPS32 registers. Each register is a 32-bit value.lo
- [Word
] The MIPS LO special register.hi
- [Word
] The MIPS HI special register.registers
- 32 general-purpose MIPS registers numbered 0 - 31. Each register contains a Word
value.A thread is represented by packing the above fields, in order, into a 166-byte buffer.
memRoot
represents the merkle root of the tree, reflecting the effects of memory writes.
-As a result of this memory representation, all memory operations are 4-byte aligned.
+As a result of this memory representation, all memory operations are WordSize
-byte aligned.
Memory access doesn't require any privileges. An instruction step can access any memory
location as the entire address space is unprotected.
For all of the following syscalls, an error is indicated by setting the return
-register ($v0
) to 0xFFFFFFFF
(-1) and errno
($a3
) is set accordingly.
+register ($v0
) to MaxWord
and errno
($a3
) is set accordingly.
The VM must not modify any register other than $v0
and $a3
during syscall handling.
The following tables summarize supported syscalls and their behaviors. If an unsupported syscall is encountered, the VM will raise an exception.
@@ -12931,7 +12952,7 @@futex_op
's FUTEX_WAIT_PRIVATE
(128) and FUTEX_WAKE_PRIVATE
(129). Other operations set errno to 0x16
.0x9
.clock_id
's REALTIME
(0) and MONOTONIC
(1). For other clock_id
's, sets errno to 0x16
. Calculates a deterministic time value based on the state's step
field and a constant HZ
(10,000,000) where HZ
represents the approximate clock rate (steps / second) of the FPVM:seconds = step/HZ
nsecs = (step % HZ) * 10^9/HZ
addr
and nsecs are set at addr + 4
.clock_id
's REALTIME
(0) and MONOTONIC
(1). For other clock_id
's, sets errno to 0x16
. Calculates a deterministic time value based on the state's step
field and a constant HZ
(10,000,000) where HZ
represents the approximate clock rate (steps / second) of the FPVM:seconds = step/HZ
nsecs = (step % HZ) * 10^9/HZ
addr
and nsecs are set at addr + WordSize
.Syscalls referencing unknown file descriptors fail with an EBADF
errno as done on Linux.
Writing to and reading from standard output, input and error streams have no effect on the FPVM state. FPVM implementations may use them for debugging purposes as long as I/O is stateless.
-All I/O operations are restricted to a maximum of 4 bytes per operation. -Any read or write syscall request exceeding this limit will be truncated to 4 bytes. -Consequently, the return value of read/write syscalls is at most 4, indicating the actual number of bytes read/written.
+All I/O operations are restricted to a maximum of WordSize
bytes per operation.
+Any read or write syscall request exceeding this limit will be truncated to WordSize
bytes.
+Consequently, the return value of read/write syscalls is at most WordSize
bytes,
+indicating the actual number of bytes read/written.
Writing to stderr/stdout standard stream always succeeds with the write count input returned, effectively continuing execution without writing work. @@ -13005,11 +13029,11 @@
As mentioned earlier in memory, all memory operations are 4-byte aligned. +
As mentioned earlier in memory, all memory operations are WordSize
-byte aligned.
Since pre-image I/O occurs on memory, all pre-image I/O operations must strictly adhere to alignment boundaries.
This means the start and end of a read/write operation must fall within the same alignment boundary.
If an operation were to violate this, the input count
of the read/write syscall must be
@@ -13028,7 +13052,6 @@