WiP PVM working-set

preamble.tex

@@ -287,6 +287,13 @@
 \newcommand*{\Cpvminitinputsize}{\mathsf{Z}_I}
 \newcommand*{\Cpvmpagesize}{\mathsf{Z}_P}
 \newcommand*{\Cpvminitzonesize}{\mathsf{Z}_Z}
+\newcommand*{\Cpvmgaspagefault}{\mathsf{G}_F}
+\newcommand*{\Cpvmgaspagealloc}{\mathsf{G}_A}
+\newcommand*{\Cpvmgaspagezero}{\mathsf{G}_Z}
+\newcommand*{\Cpvmgaspagecopy}{\mathsf{G}_C}
+\newcommand*{\Cpvmgasdeliver}{\mathsf{G}_D}
+\newcommand*{\Cpvmminworkingset}{\mathsf{W}_{\text{min}}}
+\newcommand*{\Cpvmmaxworkingset}{\mathsf{W}_{\text{max}}}
 \newcommand*{\Cgasunknown}{\mathsf{M}_\none}
 \newcommand*{\CgasG}{\mathsf{M}_G}
 \newcommand*{\CgasGeminiconst}{\mathsf{M}_{\Gemini,c}}
@@ -362,6 +369,7 @@
 \newcommand*{\Z}{\mathbb{Z}}
 \newcommand*{\zerohash}{\hash[0]}
 \newcommand*{\valcount}{\mathbb{V}}
+\newcommand*{\workingsetsize}{\mathbb{w}}
 
 %%%%%%%%%%%%
 % Blob and bitstring
@@ -478,13 +486,22 @@
 \newcommand*{\ram}{\mathbb{M}}
 \newcommand*{\ram¬value}{\mathbf{v}}
 \newcommand*{\ram¬access}{\mathbf{a}}
+\newcommand*{\ram¬frames}{\mathbf{f}}
+\newcommand*{\frame¬present}{\top}
+\newcommand*{\frame¬missing¬zero}{\bot_{\mathrm{z}}}
+\newcommand*{\frame¬missing¬copy}{\bot_{\mathrm{c}}}
+
+\newcommand*{\pageid}{\mathbb{p}}
+\newcommand*{\pid¬machine}{m}
+\newcommand*{\pid¬index}{i}
 
 \newcommand*{\workpackage}{\mathbb{P}}
 \newcommand*{\wpX}{\mathbf{p}}
 \newcommand*{\wp¬authtoken}{\mathbf{j}}
 \newcommand*{\wp¬authcodehost}{h}
 \newcommand*{\wp¬authcodehash}{u}
 \newcommand*{\wp¬authconfig}{\mathbf{f}}
+\newcommand*{\wp¬authworkingsetsize}{w}
 \newcommand*{\wp¬context}{\¬context}
 \newcommand*{\wp¬workitems}{\mathbf{w}}
 % derived fields
@@ -498,6 +515,7 @@
 \newcommand*{\wi¬codehash}{\¬codehash}
 \newcommand*{\wi¬payload}{\¬payload}
 \newcommand*{\wi¬refgaslimit}{g}
+\newcommand*{\wi¬refworkingsetsize}{w}
 \newcommand*{\wi¬accgaslimit}{a} % O/L ¬authorizer
 \newcommand*{\wi¬exportcount}{\¬exportcount}
 \newcommand*{\wi¬importsegments}{\mathbf{i}}
@@ -572,6 +590,7 @@
 \newcommand*{\sa¬gratis}{f}
 \newcommand*{\sa¬minaccgas}{g}
 \newcommand*{\sa¬minmemogas}{m}
+\newcommand*{\sa¬accworkingsetsize}{w}
 \newcommand*{\sa¬codehash}{c} % Inconsistent with ¬codehash
 \newcommand*{\sa¬balance}{b}
 \newcommand*{\sa¬created}{r}
@@ -844,6 +863,7 @@
 \newcommand*{\gaschargedflag}{\tilde{\gascounter}}
 \newcommand*{\registers}{\varphi}
 \newcommand*{\memory}{\mu}
+\newcommand*{\workingset}{\mathfrak{w}}
 \newcommand*{\pvmreg}{\N_R}
 
 \newcommand*{\segoff}{\varsigma}
@@ -854,6 +874,9 @@
 \newcommand*{\contextmutator}[1]{\Omega\ang{#1}}
 \newcommand*{\fnmemgas}{\mathcal{G}}
 
+\newcommand*{\wscharge¬internal}{\Theta}
+\newcommand*{\wscharge¬extwrite}{\Theta^{\downarrow}}
+
 %%%%%%%%%%%%
 % Other stuff
 

text/accounts.tex

@@ -8,7 +8,7 @@ \section{Service Accounts}\label{sec:accounts}
   \accounts &\in \dictionary{\serviceid}{\serviceaccount}
 \end{align}
 
-The service account is defined as the tuple of storage dictionary $\sa¬storage$, preimage lookup dictionaries $\sa¬preimages$ and $\sa¬requests$, code hash $\sa¬codehash$, balance $\sa¬balance$ and gratis storage offset $\sa¬gratis$, as well as the two code gas limits $\sa¬minaccgas$ \& $\sa¬minmemogas$. We also record certain usage characteristics concerning the account: the time slot at creation $\sa¬created$, the time slot at the most recent accumulation $\sa¬lastacc$ and the parent service $\sa¬parent$. Formally:
+The service account is defined as the tuple of storage dictionary $\sa¬storage$, preimage lookup dictionaries $\sa¬preimages$ and $\sa¬requests$, code hash $\sa¬codehash$, balance $\sa¬balance$ and gratis storage offset $\sa¬gratis$, the two code gas limits $\sa¬minaccgas$ \& $\sa¬minmemogas$, and the working-set size for accumulation $\sa¬accworkingsetsize$. We also record certain usage characteristics concerning the account: the time slot at creation $\sa¬created$, the time slot at the most recent accumulation $\sa¬lastacc$ and the parent service $\sa¬parent$. Formally:
 \begin{align}\label{eq:serviceaccount}
   \serviceaccount \equiv \tuple{\ \begin{aligned}
     \sa¬storage &\in \dictionary{\blob}{\blob}\,,\
@@ -19,6 +19,7 @@ \section{Service Accounts}\label{sec:accounts}
     \sa¬balance \in \balance\,,\
     \sa¬minaccgas \in \gas\,,\\
     \sa¬minmemogas &\in \gas\,,\
+    \sa¬accworkingsetsize \in \workingsetsize\,,\
     \sa¬created \in \timeslot\,,\
     \sa¬lastacc \in \timeslot\,,\
     \sa¬parent \in \serviceid\\

text/definitions.tex

@@ -47,6 +47,7 @@ \subsubsection{Custom Notation}
   \item[$\implications$] The set representing implications of accumulation. See equation \ref{eq:implications}.
   \item[$\ram$] The set of \textsc{pvm} $\mathbb{M}$emory (\textsc{ram}) states. See equation \ref{eq:pvmmemory}.
   \item[$\acconeout$] The set of single-service accumulation $\mathbb{O}$utputs. See equation \ref{eq:acconeout}.
+  \item[$\pageid$] The set of \textsc{pvm} memory $\mathbb{p}$age identifiers. See equation \ref{eq:pageid}.
   \item[$\workpackage$] The set of work-$\mathbb{P}$ackages. See equation \ref{eq:workpackage}.
   \item[$\workreport$] The set of work-$\mathbb{R}$eports. See equation \ref{eq:workreport}. \emph{Note used for the set of real numbers.}
   \item[$\partialstate$] The set representating a portion of overall $\mathbb{S}$tate, used during accumulation. See equation \ref{eq:partialstate}.
@@ -58,6 +59,7 @@ \subsubsection{Custom Notation}
   \item[$\edsignature{k}{m}$] The set of $\mathbb{V}$alid Ed25519 signatures of the key $k$ and message $m$. A subset of $\blob[64]$. See section \ref{sec:cryptography}.
   \item[$\bssignature{k}{c}{m}$] The set of $\mathbb{V}$alid Bandersnatch signatures of the public key $k$, context $c$ and message $m$. A subset of $\blob[96]$. See section \ref{sec:cryptography}.
   \item[$\bsringproof{r}{c}{m}$] The set of $\mathbb{V}$alid Bandersnatch Ring\textsc{vrf} proofs of the root $r$, context $c$ and message $m$. A subset of $\blob[784]$. See section \ref{sec:cryptography}.
+  \item[$\workingsetsize$] The set of valid $\mathbb{w}$orking-set sizes. See equation \ref{eq:workingsetsize}.
   \item[$\workitem$] The set of $\mathbb{W}$ork items. See equation \ref{eq:workitem}.
   \item[$\defxfer$] The set of deferred transfers. See equation \ref{eq:defxfer}.
   \item[$\avspec$] The set of availability specifications. See equation \ref{eq:avspec}.
@@ -246,6 +248,7 @@ \subsubsection{Virtual Machine components}
   \item[$\memory$] The memory sequence; a member of the set $\ram$.
   \item[$\gascounter$] The gas counter.
   \item[$\registers$] The registers.
+  \item[$\workingset$] The working-set of resident page identifiers. See appendix \ref{sec:workingsetchanges}.
   \item[$\zeta$] The instruction sequence.
   \item[$\varpi$] The sequence of basic blocks of the program.
   \item[$\imath$] The instruction counter.
@@ -292,6 +295,13 @@ \subsubsection{Constants}
   \item[$\Cmaxpackageexports = 3,072$] The maximum number of exports in a work-package. See equation \ref{eq:limitworkpackagebandwidth}.
   \item[$\mathsf{X}$] Context strings, see below.
   \item[$\Cepochtailstart = 500$] The number of slots into an epoch at which ticket-submission ends. See sections \ref{sec:slotkeysequence}, \ref{sec:epochmarker} and \ref{sec:safrolextandtickets}.
+  \item[$\Cpvmgaspagealloc = 300$] The gas cost of provisioning (and eventually deallocating) a physical frame for a \textsc{pvm} \textsc{ram} page. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgaspagecopy = 300$] The gas cost of populating a freshly provisioned \textsc{pvm} \textsc{ram} page from its initial image. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgasdeliver = 500$] The gas cost, per 1024 octets, of the eventual read-back, from the node's state or context, of data that a host-call writes into a machine's \textsc{ram}. See appendix \ref{sec:generalfunctions}.
+  \item[$\Cpvmgaspagefault = 1000$] The base gas cost of inserting a page into the \textsc{pvm} working-set. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgaspagezero = 200$] The gas cost of zero-filling a freshly provisioned \textsc{pvm} \textsc{ram} page. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmmaxworkingset = 7168$] The maximum \textsc{pvm} working-set size, in pages. See equation \ref{eq:workingsetsize}.
+  \item[$\Cpvmminworkingset = 16$] The minimum \textsc{pvm} working-set size, in pages. See equation \ref{eq:workingsetsize}.
   \item[$\Cpvmdynaddralign = 2$] The \textsc{pvm} dynamic address alignment factor. See equation \ref{eq:jumptablealignment}.
   \item[$\Cpvminitinputsize = 2^{24}$] The standard \textsc{pvm} program initialization input data size. See equation \ref{sec:standardprograminit}.
   \item[$\Cpvmpagesize = 2^{12}$] The \textsc{pvm} memory page size. See equation \ref{eq:pvmmemory}.

text/merklization.tex

@@ -87,6 +87,7 @@ \subsection{Serialization}
     \forall \kv{s}{\saX} \in \accounts: &&C(255, s) &\mapsto \encode{
       0,
       \saX_\sa¬codehash,
+      \encode[2]{\saX_\sa¬accworkingsetsize},
       \encode[8]{
         \saX_\sa¬balance,
         \saX_\sa¬minaccgas,

text/overview.tex

@@ -152,13 +152,14 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
       &\blob,\,\ \ &&\pvmreg\\
       &\gas,\,\ \ &&\bool\\
       &\sequence[13]{\pvmreg},\,\ \ &&\ram\\
+      &\optional{\N},\,\ \ &&\sequence{\optional{\pageid}}\\
     \end{alignedat}
   \,}
   \to
   \tuple{\,
     \begin{aligned}
       &\set{\halt, \panic, \oog} \cup \set{\fault,\host} \times \pvmreg, \pvmreg,\\
-      &\gas,\ \ \ \bool,\ \ \ \sequence[13]{\pvmreg},\ \ \ \ram
+      &\gas, \bool, \sequence[13]{\pvmreg}, \ram, \sequence{\optional{\pageid}}
     \end{aligned}
   \,}
 \end{equation}
@@ -176,19 +177,26 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 \begin{align}\label{eq:pvmmemory}
   \ram &\equiv \tuple{
     \isa{\ram¬value}{\blob[2^{32}]},
-    \isa{\ram¬access}{\sequence[p]{\set{\text{W}, \text{R}, \none}}}
-  }\,,\ p = \frac{2^{32}}{\Cpvmpagesize}\\
+    \isa{\ram¬access}{\sequence[p]{\set{\text{W}, \text{R}, \none}}},
+    \isa{\ram¬frames}{\sequence[p]{\set{\frame¬present, \frame¬missing¬zero, \frame¬missing¬copy}}}
+  }\\
+  p &= \frac{2^{32}}{\Cpvmpagesize} \notag\\
   \Cpvmpagesize &= 2^{12}
 \end{align}
 
-The \textsc{pvm} assumes a simple pageable \textsc{ram} of 32-bit addressable octets situated in pages of $\Cpvmpagesize = 4096$ octets where each page may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\ram$ includes two components: a value $\ram¬value$ and access $\ram¬access$. If the component is unspecified while being subscripted then the value component may be assumed. Within the context of the virtual machine, $\memory \in \ram$ is typically used to denote \textsc{ram}.
+The \textsc{pvm} assumes a simple pageable \textsc{ram} of 32-bit addressable octets situated in pages of $\Cpvmpagesize = 4096$ octets where each page may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\ram$ includes three components: a value $\ram¬value$, access $\ram¬access$, and frames $\ram¬frames$. If the component is unspecified while being subscripted then the value component may be assumed. The frames component records, per page, whether a physical frame has been allocated for it ($\frame¬present$) by the working-set gas model of appendix \ref{sec:workingsetchanges}, or, if not, whether first provisioning one would require copying the page from the program's initial image ($\frame¬missing¬copy$) or merely zeroing it ($\frame¬missing¬zero$). It influences gas costs only and has no effect on the semantics of reads and writes. Within the context of the virtual machine, $\memory \in \ram$ is typically used to denote \textsc{ram}.
 \begin{align}
   \readable{\memory} &\equiv \set{\build{i}{\memory_\ram¬access\subb{\floor{\nicefrac{i}{\Cpvmpagesize}}} \ne \none}} \\
   \writable{\memory} &\equiv \set{\build{i}{\memory_\ram¬access\subb{\floor{\nicefrac{i}{\Cpvmpagesize}}} = \text{W} }}
 \end{align}
 
 We define two sets of indices for the \textsc{ram} $\memory$: $\readable{\memory}$ is the set of indices which may be read from; and $\writable{\memory}$ is the set of indices which may be written to.
 
+On contemporary CPUs, memory is accessed via a series of caches, with increasing capacity but also increasing access latency at each level. In order to be able to accurately predict memory access latency in the gas cost model, the size of the \emph{working-set} of memory pages $\workingset \in \sequence{\optional{\pageid}}$ is constrained. The size is chosen at machine creation time from the set $\workingsetsize$, with a smaller working-set, capable of fitting in a lower-level cache, reducing the predicted latency and thus effective gas cost of each memory access. Every change to the working-set, although automatic and thus mostly invisible to the \textsc{pvm} programmer, incurs a significant gas cost. The smaller the working-set, the more likely each memory access is to ``miss'' and require such a change. The working-set size should be carefully chosen to balance these two factors. The working-set covers data, jump-table, and also code pages.
+\begin{equation}\label{eq:workingsetsize}
+    \workingsetsize \equiv \set{\build{n \in \N}{\Cpvmminworkingset \le n \le \Cpvmmaxworkingset}}
+\end{equation}
+
 Invocation of the \textsc{pvm} has an exit-reason as the first item in the resultant tuple. It is either:
 \begin{itemize}
   \item Regular program termination caused by an explicit halt instruction, $\halt$.