A Typed Programmatic Interface to Contracts on the Blockchain

Thi Thu Ha Doan0000-0001-7524-4497Peter Thiemann0000-0002-9000-1239

Ha Doan, P. Thiemann

University of Freiburg, Germany

Smart contract applications on the blockchain can only reach their full potential if
they integrate seamlessly with traditional software systems via a
programmatic interface. This interface should provide for
originating and invoking contracts as well as observing the state of
the blockchain. We propose a typed API for this
purpose and establish some properties of the combined
system. Specifically, we provide an execution model that
enables us to prove type-safe interaction between programs and the
blockchain. We establish further properties of the model that
give rise to requirements on the API. A prototype of the interface
is implemented in OCaml for the Tezos blockchain.

§ INTRODUCTION

First generation blockchains were primarily geared towards supporting
cryptocurrencies. Bitcoin is the most prominent system of this kind
[14]. Although Bitcoin already features a
rudimentary programming language called Script, second generation
blockchains like Ethereum [5] feature
Turing-complete programming facilities, called
smart contracts. They provide robust trustworthy distributed computing
facilities even though the programs run on a peer-to-peer network with
untrusted participants. Each peer in the network runs the same program
and uses cryptographic methods to check the results among the other
peers and to create a persistent ledger of all transactions, the
blockchain, thus ensuring the integrity of the results. Third
generation blockchains, like Tezos [8], are adaptable to
new requirements without breaking participating peers (no  “soft
forks” required and “hard forks” can be avoided).

The strength of programs on the blockchain is also their
weakness. They are fully deterministic in that they can only depend on
data that is ultimately stored on the chain including the parameters
of a contract invocation. Moreover, the code, the data, as well as all
transactions are public. These properties make it hard to react to
external stimuli like time triggers or events like a price exceeding a
threshold unless these stimuli get translated to
contract invocations.

Arguably, smart contracts are more useful if they can be
integrated with traditional software systems and thus triggered from
outside the blockchain.  Oracles
[13, 6] provide an approach for
contracts to obtain outside information. A contract registers a
request and a callback with an oracle. The oracle invokes the callback
as soon as an answer is available.

There are other usecases for connecting a contract with traditional software. One example is
automating procedures like managing an auction,  bidding in
an auction, optimizing fees, or initiating delivery of goods to a
customer. While some of these procedures are amenable to
implementation as contracts, we might want to save the fee of running
them on the blockchain. In particular, for actions that happen
strictly within a single domain of trust, it is not worth running them
on the blockchain. For example, automated bidding runs on behalf of
a single peer.

Building such automation requires a programmatic interface to implement the interactions.
Current blockchains mostly provide RPC interfaces,
such as the Ethereum JSON-RPC API [7] and the Tezos RPC API [8], but they
require cumbersome manipulation of string data in JSON format and do
not provide static guarantees (except that the response to a
well-formed JSON input is also a well-formed JSON output).
To improve on this situation
we present a typed API for invoking contracts from OCaml programs.
Our typed API supports the implementation of application programs and oracles
that safely interact with smart contracts on the blockchain.
Moreover, our approach provides a type-safe facility to communicate
with contracts where data is automatically marshalled between OCaml
and the blockchain. This interface is a step towards a seamless
integration of contracts into traditional programs.

§.§.§ Contributions

* A typed API for originating and invoking contracts as well as
querying the state of the blockchain.

* An operational semantics for functional programs running
alongside smart contracts in a blockchain.

* Established various properties of the combined system with
proofs in upcoming techreport.

* An implementation of a low-level OCaml-API to the Tezos
blockchain, which corresponds to the operational semantics.[
Available at <https://github.com/tezos-project/Tezos-Ocaml-API>.]

There is an extended version of the paper with further
proofs.[Available at <https://arxiv.org/abs/2108.11867>.]

§ MOTIVATION

Suppose you want to implement a bidding strategy for an auction that
is deployed on the blockchain as a smart contract.
Your bidding strategy may start at a certain amount and increase the bid until a
limit is reached. Of course, you only want to increase your bid if
someone else placed a higher bid. So you want to write a
program to implement this strategy.

This task cannot be implemented as a smart contract without
cooperation of the auction contract because it reacts
on external triggers.
Bidding requires watching the current highest bid of the contract and
react if another bidder places a higher bid.
The auction contract could anticipate the need for such observations
by allowing bidders to register callbacks that are invoked when a
higher bid arrives. However, we cannot assume such cooperation of the
auction contract nor would we be willing to pay the the fee for running
that callback.

[language=michelson,numbers=none,float=tp,caption=Header of the auction contract,label=lst:auction-contract-header,captionpos=b,emph=close,bid,emphstyle=]
parameter (or (unit
storage (pair bool          # bidding allowed
(pair address      # contract owner
address           # highest bidder's address

[language=Caml,float=tp,caption=Getting the auction handle,label=lst:getting-auction-handle,numbers=none]
# let auction = Cl.make_contract_hash auction_hash
#      parameter:(Ct.Or (Ct.Unit, Ct.Unit))
#      storage:(Ct.Pair (Ct.Bool, Ct.Pair (Ct.Addr, Ct.Addr))));;
val auction :
((unit, unit) Either.t,
bool * (Cl.Addr.t * Cl.Addr.t)) Cl.contract

[language=Caml,float=tp,caption=Bidding strategy,label=lst:bidding-strategy,numbers=none]
let rec poll limit step =
let (bidding, (_, highest_bidder)) = Cl.get_storage auction;
let high_bid = Cl.get_balance auction;
if bidding        high_bid < limit then
(if highest_bidder <> my_address then  (* entrypoint
Cl.call_contract auction
(right (min (high_bid + step, limit)))
| Cl.FAILWITH message -> poll limit step;
Time.sleep(5 * 60);
poll limit step)

For concreteness, Listing <ref> shows the
header of an auction contract in Michelson [12]. The
/parameter/ clause specifies the contract's parameter
type. It is a sum type (indicated by /or/) and each
alternative constitutes an entrypoint, named /
/left/ or /right/ summand. Both entrypoints take a /unit/
parameter. The /
tokens as the bid.
The /storage/ clause declares the state of the contract,
which is a nested pair type indicating whether bidding is allowed
(/bool/), the address of the contract owner (to prohibit
unauthorized calls to /
address. The highest bid corresponds to the token balance of the contract.

We only outline the implementation of the entrypoints. The
against the owner's address in the store. Then it transfers the funds
to the owner, closes the contract by clearing the bidding flag, and
leaves it to the owner to deliver the
goods.[For simplicity we elide safeguarding by a third-party oracle.]
The /
than the existing highest bid. Otherwise, it keeps the funds
transferred, returns the previous highest bid to its owner, and stores
the current bidder as the new highest bidder.

We present a program that implements
strategic bidding by interacting with the
blockchain.  The bidding strategy cannot be implemented as a smart

In Listing <ref>, we use the library function
!Cl.make_contract_from_hash! to
obtain a typed handle for the contract.[!Cl! is the module containing the contract
library.] The function
takes the hash of the contract along with representations of
the types of the parameter and the storage (from module
!Ct!). It checks the validity of the hash and the types with
the blockchain and returns a typed
handle, which is indexed with OCaml types corresponding to parameter
and storage type.

The implementation of the bidding strategy in Listing <ref> first checks the state of the
contract to find the current highest bid. As long as bidding is
allowed and the current bid is below our /limit/, we update
our bid by a given amount /step/, and then keep watching the state of the contract by
polling it every five minutes.

The functions /get_storage/ and /get_balance/
obtains the storage and current balance, respectively, of a contract from
the blockchain. They never fail. Function /call_contract/
takes a typed handle and a parameter of suitable type. It indicates
failure by raising an exception. If failure is caused by the
/FAILWITH/ instruction in the contract, then the
corresponding /Cl.FAILWITH/ exception is raised, which
carries a string corresponding to the argument of the instruction. In
our particular example, the auction may fail with signaling the message
/"closed"/ or /"bid too low"/. Our
code ignores this message for simplicity.

This code is idealized in several respects. Originating or running a contract requires proposing a fee to the blockchain, which may or may not be
Starting a contract may also time out for a variety of reasons. So just
invoking a contract with a fixed fee does not guarantee the contract's
execution.  Even if the invocation is locally accepted, it still takes
a couple of cycles before we can be sure the invocation is globally
accepted and incorporated in the blockchain.
Hence, after starting the invocation, we have to observe the fate of
this invocation. If it does not get incorporated, then we need to
analyze the reason and react accordingly. For example, if the
invocation was rejected because of an insufficient fee, we might want
to restart with an increased fee. Or we might decide to wait until the
invocation goes through without increasing the fee.

Hence, we would implement a scheme similar to
the bidding strategy: start with a low fee and increase (or wait) until the
contract is accepted or a fee cap is reached. On the other hand, an
observer function like /get_state/ always succeeds.

The low-level interface that we propose in this paper requires the
programmer to be explicit about fees, waiting, and polling the state
of contract invocations.

In summary, a useful smart-contract-API  has facilities to

* query the current state of the blockchain (e.g., fees in the
current block),

* query storage and balance of a contract (to obtain
the current highest bid),

* originate contracts, invoke contracts, and initiate
transfers. Hence, the API has to run on
behalf of some account (by holding its private key).

These facilities are supported by the (untyped) RPC interface of the Tezos
blockchain, which is the basis of our implementation.

§ EXECUTION MODEL

The context of our work is the Tezos blockchain
[8, 2]. Tezos is a self-amending
blockchain that improves several aspects compared to established
blockchains. Tezos proposes an original consensus algorithm,
Liquid Proof of Stake, that applies not only to the state of
its ledger, like Bitcoin [14] or Ethereum
[5], but also to upgrades of the protocol and the software.

Tezos supports two types of accounts: implicit accounts, which
are associated with a pair of private/public keys, and smart
contracts, which are programmable accounts created by an origination
operation. The address of a smart
contract is a unique public hash that depends on the creation
operation. No key pair is associated with a smart contract. An
implicit account is maintained on the blockchain with
its public key and balance.

A smart contract account is stored with its script, storage,
and balance. A contract script maps a pair of a parameter and a
storage, which have fixed and monomorphic types, to a pair of a list of
internal operations and an updated storage. An account can
perform three kinds of transactions: (1) transfer tokens to an
implicit account, (2) invoke a smart contract, or (3) originate a new
smart contract. A contract origination specifies the script of the
contract and the initial contents of the contract storage, while a
contract invocation must provide input data. Each transaction contains
a fee to be paid either by payment to a baker or by destruction
(burning). A transaction is injected into the blockchain network via a
node, which then validates the transaction before submitting it to the
network. A transaction may be rejected by the node for a
number of reasons. After validation, the transaction is injected into
a mempool, which contains all pending transactions before they can
be included in a block. A pending transaction may simply disappear
from the mempool, for example, a transaction times out when 60 blocks
have passed and it can no longer be included in a block. When a transaction
is included in the blockchain, the affected accounts are updated
according to the transaction result.

The execution model consists of functional (OCaml) programs that
interact with an abstraction of the Tezos blockchain
[8]. As the blockchain is realized by a
peer-to-peer network of
independent nodes, interaction happens through
local nodes that receive requests to originate and invoke
contracts from programs that run on a particular node. We model the blockchain
itself as a separate, abstract global entity that represents the
current consensual state of the system. Our model does not express
low-level details, but relies on nondeterminism to describe
the possible behaviors of the system. In particular, we do
not formalize the execution of the smart contracts
themselves, we rather consider them as black boxes and probe their
observable behavior. Tezos's smart contract language Michelson and its
properties have been formalized elsewhere [4].

We write $\emptyset$ for the empty set and $\mathbf{e :: s}$ to
decompose a set nondeterministically into an element $\mathbf{e}$ and a set
$\mathbf{s}$. We generally use lowercase boldface for metavariables
ranging over values of a certain syntactic category, e.g.,  for
public keys, and the capitalized name for the
corresponding type as well as for the set of these values (as in ).

§.§ Local Node

A local node runs on behalf of authorities, which are called
accounts in Tezos. An account is represented by a key pair $\Angle{
\PAK, \PUK
} $, where $\PAK$ is a private key and $\PUK$ the corresponding public
key in a public key encryption scheme.

The local node offers operations to transfer tokens from one account
to another, to invoke a contract, and to originate a contract on the blockchain.

\begin{align*}
\OP &::= \TRANSFER[\PARAMETER]\NTEZ\PUK\ADDR\MTEZ
\\&\mid \ORIGINATE\NTEZ\PUK\CODE\INIT\MTEZ
\end{align*}

In the transfer, which also serves as contract invocation,  is the amount of tokens transferred,  is the public key of the
sender,  is either a public
key for an implicit account (in case of a simple transfer)  or a
public hash for a smart contract (for an invocation),  is
the argument passed to the smart contract,
which is empty for a simple transfer, and  is
the amount of tokens for the transaction fee. In originate,   is
the script of a smart contract and  is the initial value of the
contract's storage. Each operation returns an operation hash
, on which we can query the status of the operation.

The local node offers several ways to query the current state of
the blockchain.
Some query operators are defined by the following grammar:

\begin{align*}
\QOP & ::=
% \GETCOUNTER\PUK
%        \mid
\GETBALANCE{}%\ADDR
\mid \GETSTATUS{}%\OPH
\mid \GETSTORAGE{}%\PUH
% \mid \GETCODE\PUH
% \mid \GETTYPE\PUH
\mid \GETCONTRACT{}%\OPH
\mid \dots
\end{align*}

We obtain the balance associated with an implicit account or a
contract by its public key or public hash, respectively; the status of
a submitted operation by its operation hash; the stored value of a
contract by its public hash; and the public hash of a contract by the
operation hash of its originating transaction.

The domain-specific types come with different guarantees. Values of
type  and  as well as  are not necessarily valid,
as there might be no contract associated with a hash / no account
associated with a public key. In contrast, a value of type
$\TCONTRACT\ \TYPE$ is a public hash that is verified to be associated
with a contract with parameter type $\TYPE$. Operation hashes are only returned from blockchain operations. As the surface language
neither contains literals of type  nor are there casts into
that type, all values of  are valid.

The state of a node is a pair
$\NODE = [ \EXPRS, \ACCOUNTS
% , \OPERATIONS
]$, where $\EXPRS$ is a
set of programs and $\ACCOUNTS \subseteq \TPAK \times \TPUK$  is a set of
implicit accounts.

\begin{align*}
\CONSTANT & ::= \INT \mid \FIX
\mid \OPH \mid \PUH \mid\PUK \mid \CODE \mid
\NTEZ \mid \SUNIT \mid \FALSE \mid \TRUE \\
\STATUS & ::= \STATUSPENDING \mid \STATUSINCLUDING (\INT) \mid
\STATUSTIMEOUT \\
\ERROR &::= \ERRPRG \mid \ERRBAL \mid \ERRCOUNT \mid \ERRFEE \mid
\ERRPUK \mid \ERRPUH \mid \ERRARG \mid \ERRINIT\\
\EXPR & :: =  \CONSTANT \mid \STATUS \mid \ERROR \mid \VARIABLE \mid \lambda \VARIABLE. \EXPR
\mid \EXPR\EXPR  %\mid \FST\ \EXPR \mid \SND\ \EXPR 	%\mid \NI \EI
\mid \EXPR\ \PLUS\ \EXPR\ \mid
% \EXPR\ \MINUS\ \EXPR\ \mid
\EXPR\ \EQUAL\ \EXPR\
% \mid  \EXPR\ \LESS\ \EXPR
\mid \EXPR\ \AND\ \EXPR\ \mid \EXPR\ \OR\ \EXPR\ \mid \NOT\ \EXPR
\\& \mid (\EXPR,\EXPR)\mid \NIL\ \mid \CONS\ \EXPR\ \EXPR \mid \LEFT\ \EXPR \mid\RIGHT\
\EXPR \mid \SOME\ \EXPR \mid \NONE
\mid \MATCH\ \EXPR\ \WITH\ \PATTERN\to\EXPR \dots
\\& \mid \RAISE\ \EXPR \mid \TRY\ \EXPR\ \EXCEPT\ \EXPR \mid \CAST\EXPR\TYPE\TYPEU
\\& \mid \QOP\  \EXPR \mid \TRANSFER[\EXPR]\EXPR\EXPR\EXPR\EXPR
\\& \mid \ORIGINATE\EXPR\EXPR\EXPR\EXPR\EXPR
% \\&\mid \CONTRACT\ \TYPE\ \EXPR
% \\& \mid \TOSTRING\ \EXPR \mid \FROMSTRING\ \TYPE\ \EXPR
\\
\PATTERN &::= \VARIABLE \mid (\PATTERN, \PATTERN) \mid \NIL \mid \CONS\ \PATTERN\ \PATTERN \mid \LEFT\ \PATTERN \mid\RIGHT\
\PATTERN \mid \SOME\ \PATTERN \mid \NONE \\
&\mid \FALSE \mid \TRUE \mid \STATUS \mid \ERROR
% \\
% \QOP & ::= \GETBALANCE{} \mid \GETSTATUS{} \mid \GETSTORAGE{} \mid \GETCODE{} \mid \GETCOUNTER{}
%        \mid \GETTYPE{}
\\[2ex]
\TYPE, \TYPEU & ::=
\TPUH \mid
\TPUK \mid
\TADDR \mid
\TCONTRACT\ \TYPE\ \TYPEU \mid
\TCODE\ \TYPE\ \TYPEU \mid
\TOPH\ \TYPE\ \TYPEU \mid
\TSTATUS \mid \TEXCEPTION \mid \TTEZ \\
& \mid \TNO \mid \TINT \mid \TUNIT \mid \TBOOL \mid \TSTRING \mid \TYPE\to\TYPEU \mid \TPAIR\ \TYPE\ \TYPEU \mid \TLIST\ \TYPE
\mid \TSUM\ \TYPE\ \TYPEU \mid \TOPTION\ \TYPE
\end{align*}

Syntax of expressions, , and types,

Queries and operations are started by closed
expressions of type unit that run on the
local node. Each program can send transactions on behalf of any
account on the local node.  Figure <ref>
defines the syntax of lambda calculus with sum, product, list, and option types, exceptions and fixpoint.
Pattern matching is the only means to decompose values, cf. . The execution model envisions off-chain programs interacting with smart contracts on the blockchain. The programs are defined using expression scripts. The off-chain scripts run on behalf of a single entity.

Domain-specific primitive types and constants  support blockchain
interaction, as well as several exceptional values collected in .
There is syntax to initiate transfers and to originate contracts as
well as for the queries. Finally, there is a type cast
$\CAST\EXPR\TYPE\TYPEU$, which we describe after discussing types. An
implementation provides all of these types and operations via a library API.

Types (also in Figure <ref>) comprise some base types as well as
functions, pairs, lists, sums, and option types. These types are
chosen to match with built-in types of Michelson.
There are domain specific types of public hashes $\TPUH$ and public keys $\TPUK$ subsumed by
a type of addresses $\TADDR$. $\TCONTRACT\ \TYPE\ \TYPEU$ is the type of
a contract with parameter type $\TYPE$ and storage type $\TYPEU$. $\TCODE\ \TYPE\ \TYPEU$
indicates a Michelson program with parameter type $\TYPE$ and storage
type $\TYPEU$. Tezos tokens have type $\TTEZ$. The type $\TOPH\ \TYPE\
\TYPEU$ signifies operation hashes
returned by blockchain operations. The parameters of the hash carry
the types when originating a contract. Otherwise, they are set to the
irrelevant type $\TNO$. We take the liberty of omitting irrelevant
type parameters, that is, we write $\TOPH$ for $\TOPH\ \TNO\ \TNO$.
Querying the status of an operation
returns a value of type $\TSTATUS$. Exceptions have type

\begin{align*}
\ECN{} & :: = \ECHOLE \mid \SC[\overline\VAL\ \ECN{}\ \overline\EXPR] \mid \RAISE\ \ECN{} \mid \TRY\ \ECN{}\ \EXCEPT\ \EXPR
\mid \MATCH\ \ECN{}\ \WITH\ \PATTERN\to\EXPR \dots
\\
\VAL & ::= \CONSTANT \mid \STATUS \mid \ERROR \mid \lambda x.\EXPR \mid(\VAL, \VAL) \mid
\NIL \mid \CONS\ \VAL\ \VAL \mid \LEFT\ \VAL \mid \RIGHT\
\VAL \mid \SOME\ \VAL\mid \NONE
\end{align*}

Evaluation contexts and values

Figure <ref> defines evaluation
contexts $\ECS$ and values $\VAL$.
Here $\SC$ ranges over the remaining syntactic constructors, which are
treated uniformly: evaluation proceeds from left to right. Values are
standard for call-by-value lambda calculus.

Type casts are only applicable to certain pairs of
types governed by a relation $\SubType$, which could also serve as a
subtyping relation. It is given by the axioms
$\inferrule{}{\TPUH \SubType \TADDR}$, $\inferrule{}{\TPUK \SubType
\TADDR}$, and $\inferrule{}{\TCONTRACT\ \TYPE\ \TYPEU \SubType \TPUH}$.
A cast from $\TYPE$ to $\TYPEU$ is only allowed
if $\TYPE \SubType \TYPEU$ (upcast) or $\TYPEU \SubType \TYPE$
(downcast). Upcasts always succeed, but downcasts may fail at run time.
In particular,  public hashes and public keys can both stand for addresses. Moreover, a smart
contract with parameter type $\TYPE$ is represented by its public hash
at run time. The corresponding downcast must check whether the public
hash is valid and has the expected parameter and storage type.

Figure <ref> presents selected typing rules for
expressions. We rely on an external typing judgment
$\JTypeCode\CODE\TYPE$ for the contract language, which we leave
unspecified, and $\JTypeValue\STRING\TYPE$ for serialized values as
stored on the blockchain. The latter judgment states $\STRING$ is
a string parseable as a value of type $\TYPE$.

_p _s
_p _s

, :'

''          '

''  (,
')  '

Typing rules for expressions (excerpt)

_3 _p _s

_3 _p _s

_1_2_3_4_5      _p _s

_p _s

Typing rules for blockchain operations and queries

§.§ Global Structures

Our execution model abstracts from the particulars of the blockchain
implementation, like the peer-to-peer structure or the distributed
consensus protocol. Hence, we represent the blockchain by a few global
entities: managers, contractors, and a pool of operations.

A manager keeps track of a single implicit account. Managers are
represented by a partial map $\MANAGERS : \TPUK \partialto \TBAL
\times \TCOU$. If $\MANAGERS (\PUK) = \Angle{\BAL, \COU}$ is defined, then  $\PUK$ is the
public key of an account, $\BAL$ is its
balance and $\COU$ is its counter whose form is a value-flag pair
$(n,b) \in \Nat\times\TBOOL$, where $n$ is the value of the counter
and ${b}$ is its flag.   The counter is used internally to serialize transactions.

A contractor manages a single smart contract. Contractors are
represented by a partial map $\CONTRACTORS : \TPUH \partialto
\TCODE \times \TIME  \times \TBAL \times  \TSTORAGE$. If $\CONTRACTORS (\PUH)$ = $\langle
\CODE,$ $\TIME, \BAL, \STORAGE \rangle $ is defined, then $\PUH$ is the
public hash of a contract,
$\CODE$ is its  code,
$\TIME$ is the time when it was accepted,
$\BAL$ is its current balance,
and $\STORAGE$ is its current storage. The hash $\PUH$ is
self-verifying as it is calculated from the fixed components $\CODE$
and $\TIME$. All time stamps will be different in our model.

When an operation is started on a node, it enters a pool as a
pending operation. A pending operation is either dismissed after some time or
promoted to an included operation, which has become a permanent part
of the blockchain.

The pool is a partial map $  \PENDING= \TOPH \partialto
\TOP\times \TTIME \times \TSTATUS$ where

\begin{align*}
\TSTATUS&= \STATUSPENDING + \STATUSINCLUDED\ \TTIME + \STATUSTIMEOUT
\end{align*}

such that
if $\PENDING(\OPH) = \langle  \OP, \TIME, \STATUS
\rangle $ is defined, then $\OPH$ is the public hash of the operation, $\OP$ is the operation, $\TIME$ is the time when the
operation was injected, and $\STATUS$ is either $\STATUSPENDING$,
$\STATUSINCLUDED\ \TIME'$, or $\STATUSTIMEOUT$.
A pool $\PENDING$ is well-formed if, for all $\OPH$, $\PENDING (\OPH) =
\Angle{\OP,\TIME, \STATUSINCLUDED\ \TIME'}$ implies $\TIME' \ge
\TIME$ and $\OPH = \GENERATEOPH (\OP, \TIME)$.

A pending operation is represented by
$\OPH \mapsto \langle  \OP, \TIME, \STATUSPENDING\rangle $.
Once the operation is accepted, it changes its status to included:
$\OPH \mapsto \langle  \OP, \TIME, \STATUSINCLUDED\ \TIME'\rangle $, where
$\TIME' \ge \TIME$ is  when the operation was included in the
blockchain.  The operation may also be dropped at any time, which is
represented by
$\OPH \mapsto \langle  \OP, \TIME, \STATUSTIMEOUT\rangle $. There are several
causes for dropping, primarily timeout or overflow of the pending
pool which is limited in size in the implementation.

In summary, the state of a blockchain is a tuple
$\BLOCKCHAIN = [\PENDING, \MANAGERS, \CONTRACTORS, \TIME]$ where
$\PENDING$ is a pool of operations, $\MANAGERS$ is a map of managers,
$\CONTRACTORS$ is a map of contractors, and $\TIME$ is the current

We often use the dot notation to project a component from a tuple. For
instance, we write $\BLOCKCHAIN.\MANAGERS$ to access the managers

A blockchain configuration has the form
$\BLOCKCHAIN[ \NODE_1, \dots, \NODE_n]$, for some $n>0$, where $\BLOCKCHAIN$ is a
blockchain and the $\NODE_i$ are local nodes, for $1\le i\le n$.
In a well-formed configuration, the accounts on the local nodes are all different and each
local account has a manager in $\BLOCKCHAIN$:

* for all $1\le i< j\le n$, $\NODE_i.\ACCOUNTS \cap
\NODE_j.\ACCOUNTS = \emptyset$;

* for all $1\le i \le n$,
$\forall a \in \NODE_i.\ACCOUNTS \implies a.\PUK \in \DOM( \BLOCKCHAIN.\MANAGERS)$.

§ OPERATIONAL SEMANTICS

The operational semantics is defined by several kinds of transitions:

* $\ExprTrans$ single-step evaluation of an expression in a local node,

* $\NodeTrans$ internal transitions of a node,

* $\BlockTrans$ transitions of the blockchain state,

* $\SystemTrans$ blockchain system transitions.

Evaluation of expressions is standard for call-by-value lambda calculus defined
using evaluation contexts
$\EC{}$. Figure <ref> shows some of the
reduction rules.

∉[F]   [F]

Select expression reduction rules (pattern matching omitted)

The internal transitions of a node are just evaluation of expressions.

[:: , ]
[' :: , ]

The remaining transitions affect a local node in the context of the
blockchain. To this end, any local node may be selected.

[:: ] '[' :: ]

[:: ]
[' :: ]

⦜, ∈

(, , , )

(, , )

(, )

(, )

(, , , )

= (, )

= []
[:: , ]
[, , , ]   [  :: , ]
[ ↦⦜, ,

(, , ),

(., ., ., .)

[:: , ]
[  :: , ]

= []

- ≤60

[↦⦜, ,
::, ,
, ]

[↦⦜, ,   :: ,

(, , , ),
(, , , ), +1]

-> 60

[↦⦜, ,
::, ,
, ]

[↦⦜, ,
:: ,
(, ., ),
, ]

Lifecycle transitions of a transaction

Figure <ref> shows the transitions to start
and finalize a contract invocation.
Node-Inject affects a local node and the blockchain. It
nondeterminstically selects a program that wants to do a transfer
operation. It
checks whether the sender of the transfer is a valid local account, whether
the balance is sufficient to pay the fee and the transferred amount,
whether there is an active transition for this sender (chkCount),
whether the public hash is associated with a smart contract on the blockchain, whether the type of the input parameter matchs with the smart contract's parameter type (chkArg), and whether the fee is
sufficient. If these conditions are fulfilled, the transition forges
an operation hash and returns it to the local node.
The pending operation enters the pool and the sender's counter is set
to indicate an ongoing transition.

We give just one example Node-Reject of the numerous
transitions that cover the cases where one of the
premises of Node-Inject is not fulfilled. Each of them
raises an exception that describes which condition was violated.

Acceptance or rejection of a pending operation happens on the
blockchain independent of any local node. In our model, these
transitions are nondeterministic so that acceptance can happen any
time in the next 60 cycles Block-Accept. Afterwards, a
pending operation can only time out Block-Timeout.
If the transaction is accepted, then the sender's counter is reset,
the balances of sender is adjusted (updSucc), the smart contract's storage and balance are updated (updConstr), and the time stamp increases.

Whereas Node-Inject and Block-Accept are
particular to the transfer operation, the timeout transition applies
to all operations. It just changes the state of the operation and
resets the sender's counter, thus rolling back the transaction.

§.§ Cast Reductions

.() =  ⦜, , ', '

[   :: , ]

[ :: , ]

.() = ⦜, ,
', ' ⇒
'  ∧'

[   :: , ]

[  :: , ]

Cast reductions (excerpt)

⦜, ∈
(, , , )

(, )

(, , , )

(, )

= (, )

=  [:: ,
]  [, , , ]
[ :: , ]  [↦⦜,
,  ::,

(,,), , ]

= (, )

[↦⦜, ,  :: , , , ] [↦⦜, ,   :: ,
(, , , ),
↦⦜, , ,  :: , +1]

() =  ⦜,

= (, )

[   :: , ]  [, , , ]
[   :: , ]   [, , , ]

Smart contract origination

.() = ⦜,
[ :: , ]   [ ::, ]

[Query-Balance-Fail] ∉(.)  [ :: ,
]  [
::, ]

Example queries

Figure <ref> contains the most interesting
example of cast reductions, from a public hash to a typed
contract. These reductions force the local node to obtain information
from the blockchain. The cast succeeds on  (`CONTRACT-YES'), if there is a
contractor for  such that the stored code has the parameter type
expected by the cast. The cast fails (`CONTRACT-NO'), if is invalid or if the types do not match.

§.§ Smart Contracts

The invocation of smart contracts is similar to a transfer, so we
elide the details. Figure <ref> contains the
transition Block-Originate to originate a smart contract. The basic scheme is similar
to the transfer. The preconditions for the operation are checked, but
there are extra preconditions for origination:  the program must be
well-formed and typed, the initial storage value must match its
type. The operation ends up in the pool in pending status.

Acceptance of origination is slightly different as for transfers as
shown in Block-Accept. We calculate the public hash  of the
contract from the code and the current time stamp and create a new
contractor at that address.

We obtain the handle of the contract through a query, once the
contract is accepted on the blockchain in
Block-Accept-Query. The query's argument is the operation
hash, which is used to obtain the code and the time stamp of its
acceptance. From this information, we can re-calculate the public

§.§ Queries

We conclude with two example transitions for a simple query in
Figure <ref>. To obtain the balance of an implicit
account , we obtain the account info from the manager and extract
the balance (Query-Balance-Implicit). If the account is
unknown, then we raise an exception
(Query-Balance-Fail). Other queries are implemented analogously.

§ PROPERTIES

Having defined our execution model, we proceed to prove properties of the combined systems that ensure type-safe interaction between programs and the blockchain.

§.§ Properties of blockchain state transitions

One interesting property we wish to prove is that the execution of a program that starts with valid references to accounts, operations, and contracts is not corrupted by a transition.

The following properties are preserved by a step on a well-formed
configuration $ [\EXPRS, \ACCOUNTS] \| \BLOCKCHAIN$:

* for all $\OPH$ in $\EXPRS$, $\OPH \in \DOM (\BLOCKCHAIN.\PENDING)$,

* for all $\PUK$ in $\EXPRS$, $\PUK \in \DOM (\BLOCKCHAIN.\MANAGERS)$,

* for all $\PUH$ in $\EXPRS$, $\PUH \in \DOM (\BLOCKCHAIN.\CONTRACTORS)$.

If $[\PENDING, \MANAGERS, \CONTRACTORS, \TIME] \BlockTrans{}
[\PENDING', \MANAGERS', \CONTRACTORS', \TIME']$, then

* $\TIME \le \TIME'$

*  $\DOM (\PENDING) \subseteq \DOM(\PENDING')$

* invariant for the pool: if  $\PENDING (\OPH) = \Angle{\OP,
\hat\TIME, \STATUS}$, then $\OPH = \GENERATEOPH (\OP,
\hat\TIME)$.

*  for all $\OPH \in \DOM(P)$, if
$\PENDING (\OPH) = \Angle{\OP,  \hat\TIME, \STATUS}$, then either

* $\PENDING'    (\OPH) = \PENDING (\OPH)$; or

* $\STATUS  = \STATUSPENDING$ and $\PENDING' (\OPH) =
\Angle{\OP, \hat\TIME, \STATUSTIMEOUT}$; or

* $\STATUS  = \STATUSPENDING$, $\TIME - \hat\TIME
\le 60 $,
$\PENDING' (\OPH) =       \Angle{\OP, \hat\TIME, \STATUSINCLUDED\
\TIME}$, and $\TIME'=\TIME+1$.

*  for all $\OPH \in \DOM(P)$ and $\PENDING (\OPH) = \Angle{\OP,  \hat\TIME, \STATUS}$,

* if $\STATUS=\STATUSPENDING$ and $\MANAGERS(\OP.\PUK) =  \Angle{\BAL, \COU}$ then
$\COU.b = \TRUE$ and $\BAL \ge \OP.\NTEZ + \OP.\MTEZ$;

* if $\STATUS=\STATUSINCLUDED\ \hat\TIME$, then $\hat\TIME<\TIME'$.

*  $ \DOM (\MANAGERS) \subseteq \DOM (\MANAGERS')$

*  for all $\PUK \in \DOM (\MANAGERS)$

if $\MANAGERS (\PUK) =
\Angle{\BAL, \COU}$,
then $\MANAGERS' (\PUK) =
\Angle{\BAL', \COU'}$ and

* if $\COU.b=\TRUE$ and $\COU'.b=\FALSE$, then $\COU.n' \in \{
\COU.n,  \COU.n+1\}$,

* otherwise $\COU.n = \COU'.n$

* If $\COU.n = \COU'.n$, then $\BAL = \BAL'$.

*  $ \DOM (\CONTRACTORS) \subseteq \DOM (\CONTRACTORS')$

* for all $\PUH \in \DOM (\CONTRACTORS)$,
$\CONTRACTORS (\PUH).\CODE = \CONTRACTORS' (\PUH).\CODE$

*  invariant for contractors:
for all $\PUH \in \DOM (\CONTRACTORS)$,

$\CONTRACTORS (\PUH)$ = $\Angle{ \CODE, \tilde\TIME, \BAL, \STORAGE}$
implies that $\PUH$ = $\GENERATEHASH (\CODE, \tilde\TIME)$.

Establishing items <ref> and <ref> relies on the preimage resistance of the
various hash functions used to calculate operation hashes and public
hashes: we always feed a fresh timestamp into the hash
functions for operations and code. Items <ref>–<ref> describe an invariant and
the lifecycle of
operations. Items <ref> and <ref> describe the lifecycle
of a transfer and items <ref> and <ref> describe
invariants for contractors. The invariants establish the
self-verifying property common of blockchain entities.

The proofs of these properties refer to all transitions with the detailed specifications of the related functions, such as chkCount and updSucc. Due to page limitations, not all transitions and their associated functions are presented in this paper, so the full proofs will be provided in an upcoming technical report. In this paper, we only provide the proofs for Proposition 2 at items 4 and 7.

After feeding into a node, the status of the operation is  according to the transition Node-Inject. This operation could either be accepted by the blockchain on the condition that the elapsed time is less than 60 ($\TIME - \hat\TIME \le 60$), and then its status is   (the transition Block-Accept) or it is timed out with the   status (Block-Timeout). When an operation is accepted or timed out, its status is never changed. Therefore, if $\PENDING (\OPH)$ = $\Angle{\OP,  \hat\TIME, \STATUS}$, then there are  three cases:

(1) if the operation's status remains the same as $\STATUS$ (still in ,  or ), then we have $\PENDING' (\OPH)$ = $\Angle{\OP,  \hat\TIME, \STATUS}$. This means $\PENDING' (\OPH)$ = $\PENDING (\OPH)$;

(2) if the operation's status is  ( = ), and then the operation is timed out, then we have $\PENDING' (\OPH)$ = $\Angle{\OP, \hat\TIME, \STATUSTIMEOUT}$ according to the transition Block-Timeout;

(3) if the operation's status is , the time condition is satisfied, and then the operation is accepted, then we have $\PENDING' (\OPH) = \Angle{\OP, \hat\TIME, \STATUSINCLUDED\ \TIME }$ and $\TIME'=\TIME +1$ because the timestamp is incremented by one according to the transition Block-Accept.

From (1), (2) and (3), the item <ref> of Proposition 2 is proved.

To prove this point, let us consider the two related functions. The function $\UPDATECOU(\MANAGERS, \PUK, \BOOLEAN)$ updates the flag of the counter of the account associated with the public key $\PUK$. Its specification is as follows:

($\PUK \mapsto \langle \BAL, (\NAT, \hat\BOOLEAN) \rangle$, ) = $\PUK \mapsto \langle \BAL, (\NAT, \BOOLEAN) \rangle $

The function $\UPDATESUCC(\MANAGERS, \PUK, \NTEZ, \MTEZ)$ updates the balance and the counter of the account associated with the public key $\PUK$. Its specification is as follows:

($\PUK \mapsto \Angle{\BAL, (\NAT, \TRUE)}$, , ) = $ \PUK \mapsto \Angle{\BAL - \NTEZ - \MTEZ, (\NAT + 1, \FALSE)}$

if $\MANAGERS (\PUK) =
\Angle{\BAL, \COU}$,
then $\MANAGERS' (\PUK) =
\Angle{\BAL', \COU'}$ and we have:

(1) $\COU.b=\TRUE$ means that the operation is injected and its status is  at the time  according to the transition Node-Inject.  After that, there are only two cases where the counter's flag is reset to False. If the operation is accepted, the counter's flag is reset ($\COU'.b=\FALSE$) according to the transition Block-Accept and the counter's value is incremented by 1 according to the specification of the function  ($\COU.n' =\COU.n+1$). In another case, if the operation is timed out, the counter's flag is also reset to False, but the value of the counter remains the same ($\COU.n' =\COU$) according to the transition Block-timeout. That is, if $\COU.b=\TRUE$ and $\COU'.b=\FALSE$, then $\COU.n' \in \{\COU.n, \COU.n+1\}$;

(2) otherwise, if the operation is still , the counter's value remains the same. This means $\COU.n = \COU'.n$;

(3) and then $\COU.n = \COU'.n$ means that the operation is either still  or  it has timed out. Therefore, the balance of the account remains the same because the balance is only changed when the operation is accepted. This means $\BAL = \BAL'$.

From (1), (2) and (3), the item <ref> of Proposition 2 is proved.

§.§ Typing related properties

To describe the typing of contracts we maintain an environment
$\Delta ::= \EmptyEnv \mid \PUH: \TYPE, \Delta$ that associates a
public hash with a type.
We define typing for blockchains, local nodes, and configurations.

(Δ) = (.)

Δ() =  _p _s

.().  _p _s

.(). _s

The type for a hash is a pair type, which coincides with the type of
the code stored at that hash. The storage at that hash has the type
expected by the code.

· _i
[, ]

If $\BLOCKCHAIN[\overline\NODE] \SystemTrans{} \BLOCKCHAIN'[\overline{\NODE'}]$ and
$\JTypeConfig\Delta {\BLOCKCHAIN[\overline\NODE]}$, then there is some
$\Delta' \supseteq \Delta$ such that
$\JTypeConfig{\Delta'}{ \BLOCKCHAIN'[\overline{\NODE'}]}$.

This lemma includes the standard preservation for the lambda calculus part.

If $\JTypeConfig\Delta{\BLOCKCHAIN[\overline\NODE]}$, then either
all expressions in all nodes are unit values or there is a
configuration $\BLOCKCHAIN'[\overline\NODE']$ such that
$\BLOCKCHAIN[\overline\NODE] \SystemTrans \BLOCKCHAIN'[\overline\NODE']$.

The consistency lemma says that all committed transactions respect the

Consider a blockchain state with $\JTypeBlockchain\Delta {[\PENDING, \MANAGERS, \CONTRACTORS,
\TIME]}$.

For all $\OPH\in\DOM (\PENDING)$,
if  $\PENDING (\OPH) =  \Angle{\OP, \hat\TIME, \STATUS}$

* if $\OP = \TRANSFER\NTEZ\PUK{\PUK'}\MTEZ$, then

$\PUK, \PUK'$ $\in$ $\DOM (\MANAGERS)$;

* if $\OP = \TRANSFER[\PARAMETER]\NTEZ\PUK\PUH\MTEZ$, then

* $\PUK \in \DOM (\MANAGERS)$ and $\PUH \in\DOM (\CONTRACTORS)$,

* $\JTypeValue\PARAMETER{ \TYPE_p}$ where $\Delta (\PUH)  =\TPAIR\ \TYPE_p\ \TYPE_s$;

* if $\OP = \ORIGINATE\NTEZ\PUK\CODE\STRING\MTEZ$ and $\STATUS = \STATUSINCLUDED\ \TIME'$, then

* $\PUK \in \DOM (\MANAGERS)$ and  $\PUH =\GENERATEHASH (\CODE, \TIME') \in \DOM (\CONTRACTORS)$,

* $\Delta (\PUH)  =\TPAIR\ \TYPE_p\ \TYPE_s$,  $\JTypeCode\CODE{
\TPAIR\ \TYPE_p\ \TYPE_s}$ and $\JTypeValue\STRING{ \TYPE_s}$.

Consider the proof of the second item of Lemma 3, which specifies the property on type for a smart contract invocation. A smart contract call  has the form []. If $\PENDING (\OPH) = \Angle{\OP, \hat\TIME, \STATUS }$, then the operation $\OP$ is injected into the node. According to the transition Node-Inject for a smart contract invocation, the public key is valid and the public hash must be associated with a smart contract on the blockchain. This means $\PUK \in \DOM (\MANAGERS)$ and $\PUH\in \DOM (\CONTRACTORS)$. Moreover, the chkArg function checks whether the type of the input parameter  matches the parameter type of the smart contract. If the casted type of the smart contract is $\Delta (\PUH) =\TPAIR\ \TYPE_p\ \TYPE_s$, then the type of the parameter  must be $\TYPE_p$. This means $\JTypeValue\PARAMETER {\TYPE_p}$. Therefore, this item is proved.

§ RELATED WORK

The inability to access external data sources limits the potential of
smart contracts. Oracles
[13, 6, 3] can help
overcome this limitation by providing a bridge between the outside
sources and the blockchain network. A blockchain oracle is used to provide external data for smart contracts. When the external data is available, an oracle invokes a smart contract with that information. The invocation can conveniently be made through a programmatic interface. There has been extensive research on providing oracle solutions for blockchain.  Adler et al
[11] propose a framework to explain blockchain
oracles and various key aspects of oracles. This framework aims to
provide developers with a guide for incorporating oracles into
blockchain-based applications. The main problems with using a blockchain oracle are the untrusted
data provided maliciously or inaccurately [1]. Ma at el
[10] propose an oracle equipped with
verification and disputation mechanisms. Similarly, Lo et al
[9] provide a framework for performing
reliability analysis of various blockchain oracle platforms.

Current blockchains such as Ethereum [5] and Tezos [8] often offer RPC APIs and use loosely structured data, such as a JSON-based format that is difficult for a programmatic program to handle. As a result, there is increasing work to provide better programmatic interfaces to blockchains. Web3.js [15] provides an Ethereum JavaScript API and offers Java Script users a convenient interface to interact with the Etherum blockchain. Later, Web3.py [16], derived from Web3.js, is developed to provide a Python library for interacting with Ethereum. Our typed API not only supports for programmatic programs, but also provides verifiable interaction with the Tezos smart contract platform.

§ CONCLUSION

We present a first step towards a typed API for smart contracts on the
Tezos blockchain. Our formalization enables us to establish basic
properties of the interaction between ordinary programs and smart
contracts. We see ample scope for future work to provide a
higher-level interface that exploits the similarities between
blockchain programming and concurrent programs. The next step will be to formalize the typing-related results. The formalization could connect with the Mi-Cho-Coq  formalization of Michelson contracts [4]. In the end, we would like to state and prove properties of a system that contains OCaml code (multi-threaded or distributed) connected to Michelson contracts on the Tezos blockchain via the typed API.

[1]
Al-Breiki, H., Rehman, M.H.U., Salah, K., Svetinovic, D.: Trustworthy
blockchain oracles: Review, comparison, and open research challenges. IEEE
Access  8,  85675–85685 (2020)

[2]
Allombert, V., Bourgoin, M., Tesson, J.: Introduction to the Tezos
blockchain. In: 2019 International Conference on High Performance Computing
Simulation (HPCS). pp. 1–10 (2019). 10.1109/HPCS48598.2019.9188227

[3]
Beniiche, A.: A study of blockchain oracles (2020)

[4]
Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a
framework for certifying Tezos smart contracts. In: Formal Methods. FM
2019 International Workshops, Revised Selected Papers, Part I. Lecture
Notes in Computer Science, vol. 12232, pp. 368–379. Springer (2019).

[5]
Buterin, V.: A next-generation smart contract and decentralized application
platform (2013), <https://ethereum.org/en/whitepaper/>

[6]
Caldarelli, G.: Understanding the blockchain oracle problem: A call for action.
Information  11(11) (2020)

[7]
Ethereum JSON-RPC API (2021),

[8]
Goodman, L.: Tezos-a self-amending crypto-ledger (2014),

[9]
Lo, S.K., Xu, X., Staples, M., Yao, L.: Reliability analysis for blockchain
oracles. Computers & Electrical Engineering  83,  106582 (2020)

[10]
Ma, L., Kaneko, K., Sharma, S., Sakurai, K.: Reliable decentralized
oracle with mechanisms for verification and disputation. In: 2019 Seventh
International Symposium on Computing and Networking Workshops (CANDARW). pp.
346–352 (2019)

[11]
Mammadzada, K., Iqbal, M., Milani, F., García-Bañuelos, L., Matulevičius,
R.: Blockchain Oracles: A Framework for Blockchain-Based Applications, pp.
19–34. Springer Verlag (09 2020)

[12]
Michelson: The language of smart contracts in Tezos,

[13]
Mühlberger, R., Bachhofner, S., Castelló Ferrer, E., Di Ciccio, C., Weber,
I., Wöhrer, M., Zdun, U.: Foundational oracle patterns: Connecting
blockchain to the off-chain world. Business Process Management: Blockchain
and Robotic Process Automation Forum p. 35–51 (2020)

[14]
Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008),

[15]
Vogelsteller, F., Kotewicz, M., Wilcke, J., Oance, M.: web3.js - Ethereum
JavaScript API, <https://web3js.readthedocs.io/en/v1.3.4/>

[16]
Vogelsteller, F., Kotewicz, M., Wilcke, J., Oance, M.: web3.py - a Python
library for interacting with Ethereum,


* Clarisó et al. [2017] Clarisó, R., González, C.A., Cabot, J.: Smart bound selection for the verification of uml/ocl class diagrams. IEEE Transactions on Software Engineering 45(4), 412–426 (2017) https://doi.org/10.1109/TSE.2017.2777830
  * Altoyan and Batory [2023] Altoyan, N., Batory, D.: On proving the correctness of refactoring class diagrams of mde metamodels. ACM Transactions on Software Engineering and Methodology 32(2), 1–42 (2023) https://doi.org/10.1145/3549541
  * Peled et al. [2002] Peled, D.A., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225–246 (2002) https://doi.org/10.25596/JALC-2002-225


# Dataset for Investigating Anomalies in Compute Clusters

Diana McSpadden<EMAIL_ADDRESS>Yasir Alanazi<EMAIL_ADDRESS>Bryan Hess
<EMAIL_ADDRESS>Laura Hild<EMAIL_ADDRESS>Mark Jones<EMAIL_ADDRESS>Yiyang Lu
<EMAIL_ADDRESS>Ahmed Mohammed<EMAIL_ADDRESS>Wesley Moore<EMAIL_ADDRESS>Jie
Ren<EMAIL_ADDRESS>Malachi Schram<EMAIL_ADDRESS>Evgenia Smirni
<EMAIL_ADDRESS>
###### Abstract

The dataset was collected for 332 compute nodes throughout May 19 - 23, 2023.
May 19 - 22 characterizes normal compute cluster behavior, while May 23
includes an anomalous event. The dataset includes eight CPU, 11 disk, 47
memory, and 22 Slurm metrics. It represents five distinct hardware
configurations and contains over one million records, totaling more than 180GB
of raw data.

††journal: arXiv

[1] organization=Thomas Jefferson National Accelerator Laboratory,
city=Newport News, state=VA 23606, country=USA

[2]organization=College of William and Mary, city=Williamsburg, state=VA
23187, country=USA

##  1 Background and Summary

Motivated by the goal to develop a digital twin of a compute cluster, the
dataset was collected using a Prometheus server [4] scraping the Thomas
Jefferson National Accelerator Facility (JLab) batch cluster used to run an
assortment of physics analysis and simulation jobs, where analysis workloads
leverage data generated from the laboratory’s electron accelerator, and
simulation workloads generate large amounts of flat data that is then carved
to verify amplitudes. Metrics were scraped from the cluster throughout May 19
- 23, 2023. Data from May 19 to May 22 primarily reflected normal system
behavior, while May 23, 2023, recorded a notable anomaly. This anomaly was
severe enough to necessitate intervention by JLab IT Operations staff.

The metrics were collected from CPU, disk, memory, and Slurm. Metrics related
to CPU, disk, and memory provide insights into the status of individual
compute nodes. Furthermore, Slurm metrics collected from the network have the
capability to detect anomalies that may propagate to compute nodes executing
the same job.

##  2 Methods

Agents on the hosts, node_exporter and prometheus-slurm-exporter, collect the
node_ (CPU, disk, and memory) and slurm_ metrics, respectively. The
node_exporter generally pulls its information from Linux’s proc and sysfs, and
prometheus-slurm-exporter from Slurm’s command-line utilities, but specifics
can be found in their (open) source code.[1, 3]

Prometheus scrapes the metrics from the exporters over the network and stores
them in a time-series database. Scrapes target every thirty seconds for Slurm
metrics and once a minute for other metrics, but samples may be missing if
hosts or their exporters are down, otherwise unable to promptly respond to
network requests (e.g. because of a saturated uplink), or unable to promptly
collect metrics (e.g. if the Slurm controller is so busy that it is not
responsive to commands).

A Python program using the prometheus-api-client [5] package queries
Prometheus and exports a selection of the information. There are two major
methods of the prometheus client object used to fetch data from the prometheus
server:

  * 1.

get_metric_range_data

  * 2.

and custom_query_range.

Both methods, when used with the MetricRangeDataFrame function, output a
pandas
DataFrame with the timestamp set as index.

The get_metric_range_data method outputs the raw readings and timestamps of
the provided metric in the interval [start_time, end_time]. The
custom_query_range method is more customizable. It evaluates the provided
query at all evaluation timestamps in the interval [start_time : end_time :
step]. At each evaluation timestamp, it has a default lookback of 5 minutes.
Over this lookback window, the most recent reading is assigned the evaluation
timestamp. Assigning all readings to a a certain timestamp is a useful
property when time allignment is required across different variables or
compute nodes. To get the cpu rates directly over a defined lookback interval
(144 seconds) for specific nodes (all farm nodes in addition to nodes A, and
B), we use the following custom query:

{rate(node_cpu_seconds_total{instance=$\sim$”farm.*—A—B” }[144s])}.

##  3 Data Records

The dataset contains directories for each of the metric types. These are
described in the following sections 3.1 \- 3.4.

###  3.1 CPU data

The CPU data files are sorted by the datetime of the recorded metric. For
example, the file ‘node_cpu_seconds_total_0.csv’ contains the first recorded
observations for an event followed by ‘node_cpu_seconds_total_1.csv’.

| __name__ | cpu | instance | job | mode | timestamp | value
---|---|---|---|---|---|---|---
0 | node_cpu_seconds_total | 0 | farm140105:9100 | node | idle | 2023-05-19 04:00:52.737999872 | 102923.11
1 | node_cpu_seconds_total | 0 | farm140105:9100 | node | iowait | 2023-05-19 04:00:52.737999872 | 781.04
2 | node_cpu_seconds_total | 0 | farm140105:9100 | node | irq | 2023-05-19 04:00:52.737999872 | 0.0
Table 1: Header and first three rows of node_cpu_seconds_total_0.csv from the
May event.

Table 1 illustrates the header and first three rows of the first CPU data file
from the May event. The value identifies the amount of time the CPU has spent
performing the specified task mode. The numbers reported are
counters/aggregates since the start of this year or the time when the system
booted in this year.

  * 1.

An unlabeled index column.

  * 2.

__name__: The description for the collected data.

  * 3.

cpu The CPU index for the indicated instance.

  * 4.

instance: The node instance on the compute cluster.

  * 5.

job: “node”.

  * 6.

mode: a type of task being performed by the CPU:

    * (a)

user: Time spent with normal processing in user mode.

    * (b)

nice: Time spent with niced processes in user mode.

    * (c)

system: Time spent running in kernel mode.

    * (d)

idle: Time spent in vacations twiddling thumbs.

    * (e)

iowait: Time spent waiting for I/O to completed. This is considered idle time
too.

    * (f)

irq: Time spent serving hardware interrupts. See the description of the intr
line for more details.

    * (g)

softirq: Time spent serving software interrupts.

    * (h)

steal: Time stolen by other operating systems running in a virtual
environment.

    * (i)

guest: Time spent for running a virtual CPU or guest OS under the control of
the kernel.

  * 7.

timestamp: the time that Prometheus collected the value.

  * 8.

value: Amount of time the CPU has spent performing the specified task mode.

###  3.2 Disk data

The disk data files are sorted by disk metric name, and the datetime of the
recorded metric, i.e. the file ‘node_disk_read_bytes_total_0.csv’ contains the
first recorded disk_read_bytes observations for an event followed by
‘node_disk_read_bytes_total_1.csv’, etc.

The following disk metrics are included in the dataset in separate files.

  * 1.

node_disk_io_now: (field 9) The only field that should go to zero. Incremented
as requests are given to appropriate struct request_queue and decremented as
they finish.
Example file name: node_disk_io_now_0.csv

  * 2.

node_disk_io_time_seconds_total: (field 10) Number of seconds spent doing
I/Os. This field increases so long as field 9 is nonzero.
Example file name: node_disk_io_time_seconds_total_0.csv

  * 3.

node_disk_io_time_weighted_seconds_total: (field 11) Weighted # of seconds
spent doing I/Os. This field is incremented at each I/O start, I/O completion,
I/O merge, or read of these stats by the number of I/Os in progress (field 9)
times the number of seconds spent doing I/O since the last update of this
field. This can provide an easy measure of both I/O completion time and the
backlog that may be accumulating.
Example file name: node_disk_io_time_weighted_seconds_total_0.csv

  * 4.

node_disk_read_bytes_total: (field 3) This is the total number of bytes read
successfully.
Example file name: node_disk_read_bytes_total_0.csv

  * 5.

node_disk_reads_completed_total: (field 1) This is the total number of reads
completed successfully.
Example file name: node_disk_reads_completed_total_0.csv

  * 6.

node_disk_reads_merged_total: (field 2) # of merged. Reads which are adjacent
to each other may be merged for efficiency. Thus two 4K reads may become one
8K read before it is ultimately handed to the disk, and so it will be counted
(and queued) as only one I/O. This field lets you know how often this was
done.
Example file name: node_disk_reads_merged_total_0.csv

  * 7.

node_disk_read_time_seconds_total: (field 4) This is the total number of
seconds spent by all reads (as measured from __make_request() to
end_that_request_last()).
Example file name: node_disk_read_time_seconds_total_0.csv

  * 8.

node_disk_writes_completed_total: (field 5) This is the total number of writes
completed successfully.
Example file name: node_disk_writes_completed_total_0.csv

  * 9.

node_disk_writes_merged_total: (field 6) # of merged. Writes which are
adjacent to each other may be merged for efficiency. This field lets you know
how often this was done.
Example file name: node_disk_writes_merged_total_0.csv

  * 10.

node_disk_write_time_seconds_total: (field 8) This is the total number of
seconds spent by all writes (as measured from __make_request() to
end_that_request_last()).
Example file name: node_disk_write_time_seconds_total_0.csv

  * 11.

node_disk_written_bytes_total: (field 7) This is the total number of bytes
written successfully.
Example file name: node_disk_written_bytes_total_0.csv

| __name__ | device | instance | job | timestamp | value
---|---|---|---|---|---|---
3808 | node_disk_io_now | md126 | farm140105:9100 | node | 2023-05-19 04:00:52.737999872 | 0.0
3809 | node_disk_io_now | md126 | farm140108:9100 | node | 2023-05-19 04:00:50.910000128 | 0.0
3810 | node_disk_io_now | md126 | farm140109:9100 | node | 2023-05-19 04:00:52.364999936 | 0.0
Table 2: Header and first three rows of node_disk_io_now_0.csv from the May
event.

Refer to field numbers in Kernel Documentation [2] for further information.

###  3.3 Memory data

Memory metrics are stored in separate files, one for each metric identified by
[METRIC_NAME].csv. Values recorded were scraped by Prometheus at the time
recorded in the CSV, and may increase or decrease. For filenames ending in
_bytes, while the underlying meminfo values are measured in kibibytes,
node_exporter has multiplied them out in order to suit the Prometheus
convention of using base units, so they are indeed bytes.

The following memory metrics are provided in the dataset:

  * 1.

node_memory_Active_anon_bytes: Subset of Active which is
“anonymous,” i.e. not backed by a filesystem.

  * 2.

node_memory_Active_bytes: Memory that has been used more recently and usually
not reclaimed unless absolutely necessary.

  * 3.

node_memory_Active_file_bytes: Subset of Active which is backed by a
filesystem.

  * 4.

node_memory_AnonHugePages_bytes: Non-file backed huge
pages mapped into user-space page tables.

  * 5.

node_memory_AnonPages_bytes: Non-file backed pages mapped into user-space
pagetables.

  * 6.

node_memory_Buffers_bytes: Relatively temporary storage for raw disk blocks
that shouldn’t get tremendously large (20 MB or so).

  * 7.

node_memory_Cached_bytes: In-memory cache for files read from the disk (the
page cache). Doesn’t include SwapCached.

  * 8.

node_memory_CmaFree_bytes: Free CMA (Contiguous Memory Allocator) pages
(bytes).

  * 9.

node_memory_CmaTotal_bytes: Total CMA (Contiguous Memory Allocator) pages
(bytes).

  * 10.

node_memory_CommitLimit_bytes: This is the total amount of memory currently
available to be allocated on the system.

  * 11.

node_memory_Committed_AS_bytes: The amount of memory presently allocated on
the system. The committed memory is a sum of all of the memory which has been
allocated by processes, even if it has not been “used” by them as of yet.

  * 12.

node_memory_DirectMap1G_bytes: Breakdown of page table sizes (1G) used in the
kernel’s identity mapping of RAM.

  * 13.

node_memory_DirectMap2M_bytes: Breakdown of page table sizes (2M) used in the
kernel’s identity mapping of RAM.

  * 14.

node_memory_DirectMap4k_bytes: Breakdown of page table sizes (4k) used in the
kernel’s identity mapping of RAM.

  * 15.

node_memory_Dirty_bytes: Memory which is waiting to get written back to the
disk.

  * 16.

node_memory_HardwareCorrupted_bytes: The amount of RAM/memory in KB, the
kernel identifies as corrupted.

  * 17.

node_memory_HugePages_Free: The number of huge pages in the pool that are not
yet allocated.

  * 18.

node_memory_HugePages_Rsvp: Short for ”reserved,” this is the number of huge
pages for which a commitment to allocate from the pool has been made, but no
allocation has yet been made. Reserved huge pages guarantee that an
application will be able to allocate a huge page from the pool of huge pages
at fault time.

  * 19.

node_memory_HugePages_Surp: Short for “surplus,” this is the number of huge
pages in the pool above the value in /proc/sys/vm/nr_hugepages.

  * 20.

node_memory_HugePages_total: The size of the pool of huge pages.

  * 21.

node_memory_Hugepagesize_bytes: The default hugepage size.

  * 22.

node_memory_Inactive_anon_bytes: Subset of Inactive which is “anonymous,” i.e.
not backed by a filesystem.

  * 23.

node_memory_Inactive_bytes: Memory which has been less recently used. It is
more eligible to be reclaimed for other purposes.

  * 24.

node_memory_Inactive_file_bytes: Subset of Inactive which is backed by a
filesystem.

  * 25.

node_memory_KernelStack_bytes: Memory consumed by the kernel stacks of all
tasks.

  * 26.

node_memory_Mapped_bytes: Files which have been mapped, such as libraries.

  * 27.

node_memory_MemAvailable_bytes: An estimate of how much memory is available
for starting new applications, without swapping. Calculated from MemFree,
SReclaimable, the size of the file LRU lists, and the low watermarks in each
zone. The estimate takes into account that the system needs some page cache to
function well, and that not all reclaimable slab will be reclaimable, due to
items being in use. The impact of those factors will vary from system to
system.

  * 28.

node_memory_MemFree_bytes: Total free RAM. On highmem systems, the sum of
LowFree+HighFree.

  * 29.

node_memory_MemTotal_bytes: Total usable RAM (i.e. physical RAM minus a few
reserved bits and the kernel binary code).

  * 30.

node_memory_Mlocked_bytes: Memory locked with mlock().

  * 31.

node_memory_NFS_Unstable_bytes: Pages which have been written to an NFS or
Lustre server, but have not been committed to stable storage.

  * 32.

node_memory_PageTables_bytes: Memory consumed by userspace page tables.

  * 33.

node_memory_Percpu_bytes; Memory allocated to the percpu allocator used to
back percpu allocations. This stat excludes the cost of metadata.

  * 34.

node_memory_Shmem_bytes: Total memory used by shared memory (shmem) and tmpfs.

  * 35.

node_memory_Slab_bytes: In-kernel data structures cache

  * 36.

node_memory_SReclaimable_bytes: Part of Slab, that might be reclaimed, such as
caches.

  * 37.

node_memory_SUnreclaim_bytes: Part of Slab, that cannot be reclaimed on memory
pressure.

  * 38.

node_memory_SwapCached_bytes: Memory that once was swapped out, is swapped
back in but still also is in the swapfile (if memory is needed it doesn’t need
to be swapped out AGAIN because it is already in the swapfile. This saves
I/O).

  * 39.

node_memory_SwapFree_bytes: Memory which has been evicted from RAM, and is
temporarily on the disk.

  * 40.

node_memory_SwapTotal_bytes: Total amount of swap space available.

  * 41.

node_memory_Unevictable_bytes: Memory allocated for userspace which cannot be
reclaimed, such as mlocked pages, ramfs backing pages, secret memfd pages etc.

  * 42.

node_memory_VmallocChunck_bytes: Largest contiguous block of vmalloc areas
which is free.

  * 43.

node_memory_VmallocTotal_bytes: Total size of vmalloc virtual address space.

  * 44.

node_memory_VmallocUsed_bytes: Amount of vmalloc area which is used.

  * 45.

node_memory_Writeback_bytes: Memory which is actively being written back to
the disk.

  * 46.

node_memory_WritebackTmp_bytes: Memory used by FUSE for temporary writeback
buffers.

| __name__ | instance | job | timestamp | value
---|---|---|---|---|---
11 | node_memory_Active_bytes | farm140105:9100 | node | 2023-05-19 04:00:52.737999872 | 11222962176.0
12 | node_memory_Active_bytes | farm140108:9100 | node | 2023-05-19 04:00:50.910000128 | 19978526720.0
13 | node_memory_Active_bytes | farm140109:9100 | node | 2023-05-19 04:00:52.364999936 | 19792236544.0
Table 3: Header and first three rows of node_memory_Active_bytes.csv from the
May event.

Table 3 illustrates the header and first three rows of the
node_memory_Active_bytes.csv. The 47 memory files included in the dataset use
the same header and file structure:

  * 1.

An unlabeled index column.

  * 2.

__name__: The filename and the description for the collected metric.

  * 3.

instance: The name of the node on the compute cluster.

  * 4.

job: “node”.

  * 5.

timestamp: The time that Prometheus collected the value.

  * 6.

value: The value of the __name__ metric for the instance at the timestamp.

###  3.4 Slurm data

The Slurm data files are grouped by the state of the CPU: Allocated, Idle,
Other and Total.

  * 1.

slurm_node_cpu_alloc.csv: Allocated CPUs, i.e. CPUs which have been allocated
to a job.

  * 2.

slurm_node_cpu_idle.csv: Idle CPUs, i.e. CPUs not allocated to a job and thus
available for use.

  * 3.

slurm_node_cpu_other.csv: Other CPUs, i.e. CPUs which are unavailable for use
at the moment.

  * 4.

slurm_node_cpu_total.csv: Total CPUS, i.e. the total number of CPUs.

| __name__ | instance | job | node | status | timestamp | value
---|---|---|---|---|---|---|---
0 | slurm_node_cpu_alloc | enpslurm21:9341 | slurm | farm140105 | mixed | 2023-05-19 04:00:47.217999872 | 42.0
1 | slurm_node_cpu_alloc | enpslurm21:9341 | slurm | farm140108 | mixed | 2023-05-19 04:00:47.217999872 | 36.0
2 | slurm_node_cpu_alloc | enpslurm21:9341 | slurm | farm140109 | mixed | 2023-05-19 04:00:47.217999872 | 34.0
Table 4: Header and first three rows of slurm_node_cpu_alloc.csv from the May
event.

Table 4 illustrates the header and first three rows of an Allocated slurm data
file. The Idle, Other, and Other CSV files use the same header and structure:

  * 1.

An unlabeled index column.

  * 2.

__name__: The description for the collected data.

  * 3.

instance: The hostname of the monitoring service.

  * 4.

job: “slurm”.

  * 5.

node: the name of the node on the compute cluster.

  * 6.

status: the state of the node for which the value column count applies at the
timestamp. Status can include the following suffixes and states:

    * (a)

Suffixes:

      * i.

*: The node is presently not responding and will not be allocated any new work. If the node remains non-responsive, it will be placed in the DOWN state (except in the case of completing, drained, draining, fail, failing nodes).

      * ii.

~: The node is presently in powered off.

      * iii.

#: The node is presently being powered up or configured.

      * iv.

!: The node is pending power down.

      * v.

%: The node is presently being powered down.

      * vi.

$: The node is currently in a reservation with a flag value of “maintenance.”

      * vii.

@: The node is pending reboot

      * viii.

^: The node reboot was issued.

      * ix.

: The node is planned by the backfill scheduler for a higher priority job.

    * (b)

States:

      * i.

allocated: nodes which has been allocated to one or more jobs.

      * ii.

allocated+: The node is allocated to one or more active jobs plus one or more
jobs are in the process of completing.

      * iii.

completing: All jobs associated with this node are in the process of
completing. This node state will be removed when all of the job’s processes
have terminated and the Slurm epilog program (if any) has terminated.

      * iv.

down: The node is unavailable for use. Slurm can automatically place nodes in
this state if some failure occurs. System administrators may also explicitly
place nodes in this state. If a node resumes normal operation, Slurm can
automatically return it to service.

      * v.

drained: The node is unavailable for use per system administrator request.

      * vi.

draining: The node is currently executing a job, but will not be allocated
additional jobs. The node state will be changed to state drained when the last
job on it completes. Nodes enter this state per system administrator request.

      * vii.

fail: these nodes are expected to fail soon and are unavailable for use per
system administrator request.

      * viii.

failing: The node is currently executing a job, but is expected to fail soon
and is unavailable for use per system administrator request.

      * ix.

future: The node is currently not fully configured, but expected to be
available at some point in the indefinite future for use.

      * x.

idle: nodes not allocated to any jobs and thus available for use.

      * xi.

inval: The node did not register correctly with the controller. This happens
when a node registers with less resources than configured in the slurm.conf
file. The node will clear from this state with a valid registration (i.e. a
slurmd restart is required).

      * xii.

maint: nodes which are currently marked with the maintenance flag.

      * xiii.

reboot_issued: A request to reboot this node has been made, but hasn’t been
handled yet.

      * xiv.

mixed: nodes that have some of their CPUs allocated while others are idle.

      * xv.

perfctrs (npc): Network Performance Counters associated with this node are in
use, rendering this node as not usable for any other jobs.

      * xvi.

planned: The node is planned by the backfill scheduler for a higher priority
job.

      * xvii.

power_down: The node is pending power down.

      * xviii.

powered_down: The node is currently powered down and not capable of running
any jobs.

      * xix.

powering_down: The node is in the process of powering down and not capable of
running any jobs.

      * xx.

powering_up: The node is in the process of being powered up.

      * xxi.

reserved: The node is in an advanced reservation and not generally available.

      * xxii.

unknown: The Slurm controller has just started and the node’s state has not
yet been determined.

  * 7.

timestamp: the time that Prometheus collected the value.

  * 8.

value: Number of CPUs in the file state with the indicated status on the node
at the timestamp.

###  3.5 Encoding of the Compute Node Hardware Configuration

Five distinct hardware configurations are represented in the dataset. The
primary distinction is the number of CPUs on the node. The hardware
configuration is encoded in the first six characters of the ‘instance’ or
‘node’ column in a CSV file. The five possible values are: [‘farm14’,
‘farm16’, ‘farm18’, ‘farm19’, ‘farm23’].

##  4 Usage Notes

While the data from May 19 - 22 characterizes normal compute cluster behavior,
and May 23 includes anomalous observations, the dataset cannot be considered
labeled data. The set of nodes and the exact start and end time affected nodes
demonstrate abnormal effects are unclear. Thus, the dataset could be used to
develop unsupervised machine-learning algorithms to detect anomalous events in
a batch cluster.

##  5 Acknowledgements

This material is based upon work supported by the U.S. Department of Energy,
Office of Science, Office of Nuclear Physics under contract DE-AC05-06OR23177.

## References

  * [1] The Prometheus Authors.  Configurable modular Prometheus exporter for various node metrics.  URL https://github.com/prometheus/node_exporter.
  * [2] Linux Kernel Organization.  Kernel Documentation.  URL https://www.kernel.org/doc/Documentation/iostats.txt.
  * [3] Victor Penso and Matteo Dessalvi.  Prometheus Slurm exporter.  URL https://github.com/vpenso/prometheus-slurm-exporter.
  * [4] Prometheus.  Overview.  URL https://prometheus.io/docs/introduction/overview/.
  * [5] Anand Sanmukhani.  Prometheus API client.  URL https://pypi.org/project/prometheus-api-client/.