Invariant <ref> captures the fact that the base level gets marked at the end. This fact is useful for us because we can combine it with $\past (\markof{\vpred, i} = \false)$ to obtain $\past (\markof{\vpred, 0} = \false)$. Since findNext has found $\vpred$ to be marked at the base level, we can determine that it got marked at some time point between the point in time when $\past (\markof{\vpred, 0} = \false)$ held and the present. Let $t$ be the time point right before $\vpred$ got marked. The following invariant gives us useful information about which node $\nextof{\vpred, 0}$ can be pointing to at time $t$:

*   For all nodes $n$ and level $i$, once $\markof{n, i}$ is set to $\true$, $\nextof{n, i}$ does not change.

Invariant <ref> preceisely says that $\nextof{\vpred, 0} = \vcurr$ at time $t$. Thus, we have found a moment in time when $\markof{\vpred} = \false$, $\keyof{\vpred} < k$ and $\nextof{\vpred, 0} = \vcurr$. These three facts allow us to immediately conclude that $k \in \insetof{\vcurr}$ at time $t$. This finally completes the proof of traverse.

§.§ Lazy Traverse

The code for the lazy traversal is shown in <Ref>. While the $\lazyRec$ implementation is almost identical to $\eagerRec$, the two differ in the per-level traversal in $\lazyI$ and $\eagerI$. The $\lazyI$ function here keeps track of three nodes while traversing: node $\vpred$ is the last unmarked node it witnessed, node $\vprednext$ is the node that $\vpred$ was pointing to when $\vpred$ was traversed, and $\vcurr$ is the node that is currently being traversed. The function $\lazyI$ begins by reading the next pointer and mark bit of $\vcurr$. If $\vcurr$ is found to be marked, then $\lazyI$ simply continues with the successor of $\vcurr$. If $\vcurr$ is unmarked, then the operation key $k$ is compared with $\keyof{\vcurr}$. In case $\keyof{\vcurr} < k$, then again $\lazyI$ continues with $\vcurr$ as the last seen unmarked node. Otherwise, $k \le \keyof{\vcurr}$. In this case, it attempts to unlink the marked segment between nodes $\vpred$ and $\vcurr$. The conditional on Line <ref> checks if there is a segment to remove. If that is indeed the case, then $\lazyI$ calls changeNext to unlink the segment between $\vpred$ and $\vcurr$. If changeNext succeeds, then there is a further check to make sure $\vcurr$ is still unmarked. If so, then $\lazyI$ returns with $\vpred$ and $\vcurr$. In all other cases where changeNext fails or $\vcurr$ is found to be marked, $\lazyI$ restarts the traverse function.

[aboveskip=0pt,belowskip=0pt, frame=none]
let $\lazyI$ $i$ $k$ $\vpred$ $\vprednext$ $\vcurr$ =
match |<findNext>| $i$ $\vcurr$ with
| $\vcurrnext$, $\true$ -> $\lazyI$ $i$ $k$ $\vpred$ $\vprednext$ $\vcurrnext$@@
| $\vcurrnext$, $\false$ ->
let $\vcurrk$ = |<getKey>| $\vcurr$ in
if $kc$ < $k$ then
$\lazyI$ $i$ $k$ $\vcurr$ $\vcurrnext$ $\vcurrnext$@@
let $\vres$ = ($kc$ = $k$ ? $\true$ : $\false$) in
if $\vprednext$ = $\vcurr$ then@@
($\vpred$, $\vcurr$, $\vres$)@@
match |<changeNext>| $i$ $\vpred$ $\vprednext$ $\vcurr$ with
| Success ->
let _, $b$ = |<findNext>| $i$ $\vcurr$ in
if $b$ then traverse $\vparr$ $\vsarr$ $k$
else ($\vpred$, $\vcurr$, $\vres$)@@
| Failure -> traverse $\vparr$ $\vsarr$ $k$

[aboveskip=0pt,belowskip=0pt, frame=none, firstnumber=last]
let $\lazyRec$ $i$ $\vparr$ $\vsarr$ $k$ =
let $\vpred$ = $\vparr$[$i$+1] in
let $\vcurr$, _ = |<findNext>| $i$ $\vpred$ in
let $\vpredp$, $\vcurrp$, $\vres$ = $\lazyI$ $i$ $k$ $\vpred$ $\vcurr$ $\vcurr$ in
$\vparr$[$i$] <- $\vpredp$;
$\vsarr$[$i$] <- $\vcurrp$;
if $i$ = 0 then
($\vpredp$, $\vcurrp$, $\vres$)
$\lazyRec$ ($i$-1) $\vparr$ $\vsarr$ $k$

let traverse $\vparr$ $\vsarr$ $k$ =
$\lazyRec$ ($\vL$ - 2) $\vparr$ $\vsarr$ $k$

The lazy traversal for the skiplist template corresponding to the Harris List style traversal.

§.§ Proof of Lazy Traversal

The proof idea for the lazy traversal is similar to that of the eager traversal.  We provide a brief overview of the traversal invariant for $\lazyI$, and why it is sufficient to establish the required specification for traverse. The following discussion focuses on the $\lazyI$ executing on the base level, for sake of simplicity.

The traversal invariant for $\lazyI$ is defined as below:

\begin{align*}
\lazyinv(k, \vpred, \vprednext, \vcurr) \defeq {} & \eagerinv(k, \vpred, \vprednext) * (\vprednext \neq \vcurr \impl \exists\; \vls.\; \markedseg(\vprednext, \vls, \vcurr))\\
\markedseg(\vprednext, \vls, \vcurr) \defeq {} & (\vls = \texttt{[]} \impl \past (\nextof{\vprednext, i} = \vcurr))\\
{} & * (\vls = \texttt{[\ensuremath{n_0},...,\ensuremath{n_l}]} \impl \past (\nextof{\vprednext, 0} = n_0) \\
{} & \hspace{9.5em} * (\forall\; 0 \le j < l.\; \past \nextof{n_j, 0} = n_{j+1}))\\
{} & \hspace{9.5em} * \past (\nextof{n_l, 0} = \vcurr)
\end{align*}

The invariant $\lazyinv$ relies on $\eagerinv$ and a new predicate $\markedseg$ that stores the segment of marked nodes. Additionally, the predicate establishes that the nodes $\vprednext$ and $\vcurr$ are the start and end points of the marked segment.

To see that $\lazyinv$ is indeed an invariant, consider Lines <ref> and <ref> where $\lazyI$ is recursively called. At Line <ref>, the marked segment can be extended by including the marked node $\vcurr$, while $\vpred$ and $\vprednext$ remain unchanged. On the other hand, at Line <ref>, the second conjunct of $\lazyinv$ becomes trivially true, and $\
eagerinv(k, \vcurr, \vcurrnext)$ can be established in the same way as for $\eagerI$.

Let us now show why $\lazyinv$ is sufficient to prove the traverse specification. Consider the points where $\lazyI$ terminates (lines <ref> and <ref>). When terminating at Line <ref>, we know that $\vprednext = \vcurr$. Hence, $\lazyinv$ provides the predicate $\eagerinv(k, \vpred, \vcurr)$. Using the same argument as $\eagerI$, we can establish the required postcondition. Now consider Line <ref>. In this case, the thread has successfully unlinked the marked segment, hence it can establish that $\markof{\vpred, 0} = \false$ and $\nextof{\vpred, 0} = \vcurr$ right after the call to changeNext. Note that the later check whether $\vcurr$ is unmarked must succeed in order for $\lazyI$ to terminate. Hence, at the point of the successful changeNext, $\vcurr$ must also be unmarked, giving us all the facts necessary to establish the required postcondition. This completes the proof of $\lazyI$.

§ SOUNDNESS OF HINDSIGHT SPECIFICATION

This section focuses on the soundness of the Hindsight specification, i.e., the proof that any structure that satisfies $(\ref{eq:hindsight-spec})$ must also satisfy $(\ref{eq:client-spec})$. We begin with some background on Iris that will be necessary for the proof, followed by additional details on the predicate $\historyinv$ and the helping invariant $\helpinginv$. Finally, we provide a proof outline relating $(\ref{eq:hindsight-spec})$ to the $(\ref{eq:client-spec})$.

§.§ Iris Primer

Iris is a state-based concurrent separation logic. Assertions in the logic express ownership of resources. These resources include both physical resources that are manipulated by the program as well as ghost resources that capture auxiliary information for the purpose of the proof and that are manipulated using the proof rules of the logic. An example of an assertion describing a physical resource is the points-to predicate, $\ell \mapsto v$, which expresses ownership of heap location $\ell$ and constrains its stored value to be $v$. Two assertions $P$ and $Q$ (e.g. describing disjoint heap regions) can be composed using aseparating conjunction, $P * Q$. The logic supports standard local reasoning principles such as the frame rule: if the Hoare triple $\hoareTriple{P}{e}{Q}$ is valid, then so is $\hoareTriple{P * R}{e}{Q * R}$ for all frames $R$.

To describe ghost resources, Iris provides assertions of the form $\ghostState{}{\melt}$ which state ownership of a chunk $\melt$ of the ghost resource stored at ghost location $\gamma$. The chunk $\melt$ must be drawn from a camera that is specified as part of the proof. Cameras generalize the partial commutative monoids that are commonly used to define the semantics of separating conjunction. The precise definition of these structures is immaterial for this paper. What is important is that a camera is a set $S$ equipped with an operation $\melt \cdot \meltB$ that is compatible with separating conjunction in the following way: $\ghostState{}{\melt} * \ghostState{}{\meltB} \provesIff \ghostState{}{\melt \raOp \meltB}$.

A simple example is the $\mathsf{MaxNat}$ camera defined by $S = \setcomp{\maxnat(n)}{n \in \Nat}$ and $\maxnat(n)\cdot\maxnat(m)=\maxnat(\max(n,m))$.

A proof can introduce ghost resources as needed by allocating a fresh ghost location $\gamma$. A proof can also update chunks of ghost resources at existing ghost locations using view shifts, $\ghostState{}{\melt} \vsR \ghostState{}{\meltB}$. A view shift is only allowed if replacing $\melt$ by $\meltB$ is frame-preserving. Intuitively, this means that for any $\meltC$ such that the full ghost resource stored at $\gamma$ may be $\melt \cdot \meltC$ before the update, $\meltB$ must also compose with $\meltC$. For example, in the $\mathsf{MaxNat}$ camera, all updates are frame-preserving because composition (maximum) is totally defined. However, in general, this is not the case.

To reduce the burden on the proof author, Iris provides a library of predefined parameterized cameras. One such camera that we will use below is the agreement camera $\Ag(X)$ which is defined for any set $X$. The elements take the form $\agree(x)$ for $x \in X$ and composition is only defined in the case of identity: $\agree(x)\cdot\agree(x)=\agree(x)$. Another predefined camera we will use is that of finite partial maps from some set $X$ to some camera $R$, $\Map(X,R)$, with composition defined by lifting the composition on $R$ pointwise to maps.

To enable reasoning about shared resources, Iris provides the notion of an invariant. Any Iris assertion $P$ can be turned into an invariant, denoted $\sinv{P}$. Once an invariant has been created, it becomes a duplicable resource, which means that it can be commonly owned by all threads. An individual thread may access (and manipulate) the resources described by the underlying assertion $P$ when performing a computation step, provided $P$ is reestablished after each step.

A reoccurring pattern in Iris proofs is to have an invariant that holds authoritative ownership of the current state of a resource, and each thread may additionally own partial knowledge about this resource that the thread gathered during its execution.
To encode this pattern, Iris provides the authoritative camera $\mathsf{Auth(R)}$ defined over any camera $R$.
The authoritative camera has elements of the form $\authAuth\; a$ to denote authoritative ownership of $a \in R$ and $\authFrag\; a$ to denote fragmental ownership. The composition $\authAuth\;a \raOp \authFrag\;b$ expresses the fact that $b$ is a fragment of $a$, i.e., $\exists\; c, a = b \raOp c$. For example, the camera $\mathsf{Auth(MaxNat)}$ is very useful to establish lower bounds of a monotonically non-decreasing quantity. The definitions of $\mathsf{Auth(MaxNat)}$ yields the valid entailment: $\ghostState{}{\authAuth\; \maxnat(n)} * \ghostState{}{\authFrag\; \maxnat(n')} \vdash n' \leq n$. The permitted frame-preserving updates are shown below:

auth-max-updn ≤n'(n) (n')

(n) (n) * (n)

The rule auth-max-upd requires that the update only increases the authoritative value to guarantee that the new authoritative value $n'$ still composes with all fragmental values.

§.§ Tracking the Computation History

Hindsight arguments involve reasoning about past program states. Our encoding therefore tracks information about past states using computation histories.

We define computation histories as finite partial maps from timestamps, $\Nat$, to snapshots, $\Snap$. A snapshot describes an abstract view of a program state at a particular time. It is a parameter of our encoding. For instance, a snapshot may capture the physical memory representation of the data structure under proof, while abstracting from the remainder of the program state.

Another parameter of our encoding is a function $\cssabs{\cdot}$ that computes the abstract state of the data structure from a given snapshot.

The predicate $\historyinv(H, T)$ consists of two ghost resources: one resource to store the authoritative computation history $H$, and one resource to store the last timestamp $T$ used in $H$. Whenever the program changes the program state in a way that is observable at the level of snapshots, the invariant forces $H$ to be updated with a new snapshot at time $T+1$, and $T$ to be increased by $1$. To track $T$, we use the camera $\mathsf{Auth(MaxNat)}$, which implicitly encodes the fact that timestamps are non-decreasing, effectively serializing the snapshot changes in the history.

We want threads to be able to own fragmental knowledge of the authoritative history $H$. These history fragments are then used to define past predicates that express the existence of a past state with a certain snapshot. To this end, we use the camera $\Auth(\Map(\Nat,\Ag(\Snap)))$ for the resource that tracks the history. The use of the agreement camera ensures that the history can only be updated by appending to it (i.e., all snapshots of past states are preserved).

Our encoding of the history must be “append-only”; i.e. past states are not allowed to change once recorded. The agreement camera is useful here. The elements of the agreement camera are of the type $\agree(\melt)$ and whose rules provide the property $\mval (\agree(\melt) \raOp \agree(\meltB)) \impl \melt = \meltB$. Furthermore, note that finite maps with piecewise composition also form a camera. Given a map $M$ from timestamps to snapshot, we define $\Ag(M)$ as the map where each entry $t \mapsto s$ is transformed to $t \mapsto \agree(s)$. The authoritative version of $\Ag(M)$ provides exactly the properties we need:

auth-agree-upd(M) ∩(M') = ∅(M) (M ∪M')

auth-agree-snapt ∈(M) M(t) = s
(M) (M) * {t := (s)}

(M) * {t := (s)} t ∈(M) M(t) = s

{t := (s)} * {t := (s')} s = s'

The rule auth-agree-upd makes history append-only, while auth-agree-snap allows a thread to take a snapshot of a past state. Rule auth-agree-frag allows a thread with a snapshot to infer that it was indeed part of history. If a thread has two snapshots from time $t$, rule auth-agree-agree says that the snapshots must be equal. This follows from underlying rules of the agreement camera.

We are finally ready to present our encoding of the history using the predicate $\historyinv(M, T)$. Here, variable $M$ is a map from timestamp to snapshots representing the history and $T \in \Nat$ representing the timestamps used so far. The authoritative ghost resource on $T$ and $M$ capture the properties that we discuss above. The domain of $M$ is $\{0 \dots T\}$. The purpose of the last conjunct is to ensure that a thread appends to the history whenever any change to the structure is made.

The predicate $\historyinv(H, T)$ is then defined as

\begin{align*}
\historyinv(H, T) \defeq {} & \ghostState{t}{\authAuth\; \maxnat(T)} \,*\, \ghostState{m}{\authAuth\; \agree(H)} \\
& {} \,*\, \dom(H) = \{0 \dots T\} \,*\,  \forall t < T.\, H(t) \neq H(t+1)\enspace.
\end{align*}

Here, we abuse notation and write $\agree(H)$ for the function that takes the history $H$ to an element of $\Auth(\Map(\Nat,\Ag(\Snap)))$ in the expected way. The second last conjunct ensures that the authoritative history contains no gaps. The purpose of the last conjunct is to ensure that a thread appends to the history whenever any change to the program state is made that affects the snapshot (see discussion in <ref>).

§.§ Augmenting op with Prophecies

In light of the discussion in <ref>, we must augment $\cssOp$ with auxiliary ghost code that creates and resolves the relevant prophecies. We do this by defining the wrapper function $\csslop$ given in <ref>.

Let us first briefly discuss how prophecy variables can be used in Iris. The right side of <ref> shows the specifications of the two functions related to manipulating prophecies.

The function $\newproph$ returns a fresh prophecy $p$ that predicts a sequence of values $pvs$, captured by the resource $\proph(p, \vpvs)$.

This resource can be owned and shared among threads via a shared invariant. The resource is also non-duplicable.

The values contained in the sequence $\vpvs$ are determined by how $p$ is resolved using the $\code{Resolve}$ command. The rule prophecy-resolution ties the observed value ($v$) to the next prophesied value (the head of $\vpvs$). It also updates $\proph(p, \vpvs)$ to the tail of $\vpvs$ for the remaining prophesied values that are yet to be observed. In our context, we want the prophecy to predict whether the decisive operations (i.e. markNode and changeNext) will succeed as well as their return value. Hence, we augment delete and insert by wrapping their decisive operations inside a Resolve command. The return value is captured by the resolution on Line <ref>. For our purposes, we assume that $\vpvs$ is a sequence of Success or Failure values (i.e., the result of each attempted call to the decisive operation) followed by a special value $\prophend{\vres}$ indicating that no further future calls are expected, and that $\vres$ will be the final return value[We have to also consider the case where $\vpvs$ is not of this form, but that is a  trivial case to handle and thus we do not consider it in this discussion.]. Given the prophesied sequence of values $\vpvs$, a thread will exhibit an unmodifying linearization point iff $\vpvs$ does not contain any Success values.

Let us now turn to $\csslop$, which starts by generating a unique thread identifier using $\newthreadid$ on Line <ref>. We also implement $\newthreadid$ using the $\newproph$ construct. There are two benefits to this: (i) Iris makes sure that prophecy identifiers are unique out of the box, and (ii) now we can use Iris's erasure theorem for prophecies to argue that the augmented code $\csslop$ has the same behavior as $\cssOp$. After, $\csslop$ creates a prophecy $p$ as described above, it invokes the underlying operation $\cssOp$, and finally, terminates after resolving $p$ to the result of $\cssOp$.

[aboveskip=0pt,belowskip=0pt, frame=none]
let $\csslop$ $r$ $k$ =
let $\tid$ = $\newthreadid$ in @@
let $p$ = $\newproph$ in @@
let $v$ = $\cssOp$ $p$ $r$ $k$ in @@
$\resolve{p}{\prophend{v}}$; $v$ @@

𝖳𝗋𝗎𝖾p.  ∃  .  (p, )

(p, )   pv
∃  .  (p, )  *  = v ::

Wrapper augmenting $\cssOp$ with prophecy-related ghost code, whose specification is given on the right.

We can now finally present the client-level specification with $\csslop$:

$$ \minvr \magicwand \atomicTriple{C.\; \cssstate(r, C)}{\csslop\;p\;r\;k}{\vres \; C'. \; \cssstate(r, C') \,*\, \dSpec{op}(k, C, C', res) }.$$

The next section provides details on our choice of $\mainInv(r)$ and the proof of $\csslop$.

§.§ Proof of $\csslop$

\begin{align*}
\minvr \defeq {} & \exists\, H\, T\, C.\; \csslstate(r, C) * \cssabs{H(T)} = C\\
{} & * \historyinv(H, T)  \,*\, \helpinginv(H, T) \,*\, \tplinv(H, T) \\
\helpinginv(H, T) \defeq {} & \exists\, R.\; \ghostState{r}{\authAuth\; R} \\
{} & * \Sep_{\tid \in R}
\; \exists\, \cssOp\, k\, v_p\, t_0\, \Phi\, \token.\; \reg(\tid, \cssOp, k, v_p, t_0, \Phi, \token) \\
\reg(\tid, \cssOp, k, v_p, t_0, \Phi, \token) \defeq {} &
\thread(\tid, t_0) * \sinv{\helpingstate(\cssOp, k, v_p, t_0, \Phi, \token)}
\\[.5em]
%\globalInt(r, \interface) \defeq {}
%& r \in \dom(\interface) \wedge \outflowOfInt{\interface} = \lambda_0
\helpingstate(\cssOp, k, v_p, t_0, \Phi, \token) \defeq {}
& \linpending(\cssOp, k, v_p, t_0, \Phi) \lor \lindone(\cssOp, k, v_p, t_0, \Phi, \token)
\\[.5em]
\linpending(\cssOp, k, v_p, t_0, \Phi) \defeq {}
{\atomicUpdate}_{\cssOp}(\Phi) * \neg \pastlin(\cssOp, k, v_p, t_0)
\\[.5em]
\lindone(\cssOp, k, v_p, t_0, \Phi, \token) \defeq {}
&  (\Phi(v_p)\; \lor\; \token) * \pastlin(\cssOp, k, v_p, t_0)
\end{align*}

Definition of the invariant encoding the helping protocol.

fig-helping-prot-inv' shows a simplified definition of the invariant that encodes the helping protocol[For presentation purposes, the proof outline presented here abstracts from some technical details of the actual proof in Iris.].

The definitions are implicitly parameterized by a proposition $\tplinv(r,H,T)$, which abstracts from the resources needed for proving that a specific structure satisfies the hindsight specification.

The helping protocol predicate $\helpinginv(H, T)$ contains a registry $\ghostState{r}{\authAuth\; R}$ of thread IDs with unmodifying linearization points that require helping from other concurrent threads.
For each thread ID $\tid$ in the registry, the shared state contains $\thread(\tid,\_)$ along with the state of $\tid$, which is either $\linpending$ or $\lindone$. $\linpending$ captures an uncommitted atomic triple, and $\lindone$ describes the operation after it has been committed. Note that we use the notation ${\atomicUpdate}_{\cssOp}(\Phi)$ to refer to the atomic update token of $\cssOp$ and write just ${\atomicUpdate}(\phi)$ when $\cssOp$ is clear.

[aboveskip=1pt,belowskip=0pt, frame=none]
$\minvr * \annotAtom{C.\; \cssstate(r,C)}$
let $\csslop$ $r$ $k$ =
$\annot{\atomicUpdate(\Phi)}$ @@
let $\tid$ = $\newthreadid$
$\annot{\atomicUpdate(\Phi) * \proph(\tid, \_)}$
let $p$ = $\newproph$ in
$\annot{\atomicUpdate(\Phi) * \proph(\tid, \_) * \proph(p, \vpvs) * \minvr}$ @@
(* Open invariant *)
$\annot{\atomicUpdate(\Phi) * \thread(\tid, T_0) * \proph(p, \vpvs) * \csslstate(r, C_0) * \helpinginv(H_0, T_0) * \dots}$
(* Case analysis on $\procProph(\vpvs)$ : only showing $\neg \procProph(\vpvs)$ *)
$\annot{\atomicUpdate(\Phi) * \thread(\tid, T_0) * \proph(p, \vpvs) * \csslstate(r, C_0) * \ghostState{r}{\authAuth\; R} * \tid \notin R * \dots}$
(* Let $v_p$ such that $\vpvs$ contains $\prophend{v_p}$ *)
(* Case analysis on $\dSpec{op}(k, \abs{H_0(T_0)}, \abs{H_0(T_0)}, v_p)$ : only showing $\neg \dSpec{op}(\abs{H_0(T_0)}, \abs{H_0(T_0)}, v_p)$ *)
$\annot{\thread(\tid, T_0) * \proph(p, \vpvs) * \csslstate(r, C_0) * \ghostState{r}{\authAuth\; R} * \tid \notin R}$ @@
$\annot{\dots * \atomicUpdate(\Phi) * \thread(\tid, T_0) * \neg \pastlin(\cssOp, k, v_p, T_0)}$
$\annot{\dots * \atomicUpdate(\Phi) * \thread(\tid, T_0) * \linpending(\cssOp, k, v_p, T_0, \Phi) * \token}$
$\annot{\dots * \helpingstate(\cssOp, k, v_p, T_0, \Phi, \token) * \token}$
(* Ghost update: $\ghostState{r}{\authAuth\; R} \vsR \ghostState{r}{\authAuth\; R \cup \set{\tid}}$ *) @@
$\annot{\thread(\tid, T_0) * \proph(p, \vpvs) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \csslstate(r, C_0) * \ghostState{r}{\authAuth\; R \cup \{tid\}} * \dots }$
$\annot{\thread(\tid, T_0) * \proph(p, \vpvs) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \csslstate(r, C_0) * \helpinginv(H_0, T_0) * \dots }$
(* Close invariant *)
$\annot{\thread(\tid, T_0) * \proph(p, \vpvs) * \ghostState{r}{\authFrag\; \{tid\}} * \token }$
let $v$ = $\cssOp$ $p$ $r$ $k$ in @@
$\annot{\thread(\tid, T_0) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \proph(p, \vpvss) * (\vpvs = \vprf \;\code{++}\; \vpvss) \\ * (\procProph(\vpvs) \magicwand \Phi(v)) * (\neg \procProph(\vpvs) \magicwand \pastlin(\cssOp, k, v_p, T_0))}$ @@
$\annot{\thread(\tid, T_0) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \proph(p, \vpvss) * \pastlin(\cssOp, k, v_p, T_0)}$
$\resolve{p}{\prophend{v}}$; @@
$\annot{\thread(\tid, T_0) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \proph(p, \code{[]}) * (v_p = v) * \pastlin(\cssOp, k, v_p, T_0)}$
(* Open invariant *)
$\annot{\thread(\tid, T_0) * \ghostState{r}{\authFrag\; \{tid\}} * \token * \pastlin(\cssOp, k, v, T_0) * \cssstate(r, C_1) * \helpinginv(H_1, T_1) * \dots}$
$\annot{\dots * \token * \ghostState{r}{\authFrag\; \{\tid\}} * \pastlin(\cssOp, k, v, T_0) * \helpingstate(\cssOp, k, v, T_0, \Phi, \token)}$
$\annot{\dots * \token * \pastlin(\cssOp, k, v, T_0) * \lindone(\cssOp, k, v, T_0, \Phi, \token)}$
$\annot{\dots * \token * \pastlin(\cssOp, k, v, T_0) * (\Phi(v) \lor \token)}$
$\annot{\dots * \Phi(v) * \pastlin(\cssOp, k, v, T_0) * (\Phi(v) \lor \token) }$
$\annot{\dots * \Phi(v) * \pastlin(\cssOp, k, v, T_0) * \lindone(\cssOp, k, v, T_0, \Phi, \token)}$
$\annot{\Phi(v) * \cssstate(r,C_1) * \helpinginv(H_1, T_1) * \dots}$
(* Close invariant *)
$\annotAtom{\vres \; C'. \; \cssstate(r, C') \,*\, \dSpec{op}(C, C', res)}$

Outline for the proof of the client-level specification for op.

The proof outline for $\csslop$ is shown in fig-op'-proof. The proof begins by creating a thread identifier $\vtid$ and prophecy $p$. As alluded to earlier, $\newthreadid$ is also just $\newproph$ in disguise, hence we obtain two prophecy resources, one each for $\vtid$ and $p$. Before we can invoke $\cssOp$, we must record the start time of this thread and perform a case split on $\procProph(\vpvs)$ to determine if this thread requires helping. For this, we open the invariant at Line <ref>. To record the start time, we give up the resource $\proph(\vtid, \_)$ to gain a duplicable resource $\thread(\vtid, T_0)$ in exchange ( $T_0$ is the current timestamp). The exact details of this exchange are not relevant, so we continue with the case split on $\procProph(\vpvs)$. First consider the case that $\procProph(\vpvs)$ holds. Then, thread $\vtid$ does not require helping and the hindsight specification can ensures that $\cssOp$ linearizes correctly. This is quite straightforward, so we focus on the other case, i.e. $\procProph(\vpvs)$ does not hold.

In order to register the thread for helping, we must establish $\pastlin(\cssOp, k, v_p, T_0)$ or its negation. Here, $v_p$ is the return value obtained by scanning for the end marker in $\vpvs$. We proceed by first checking if the thread can be linearized at the current timestamp $T_0$. If so, then we can safely linearize the thread right away. So let us focus on the more interesting case where we cannot linearize right away (Line <ref>). Here, the thread registers itself with the helping protocol by updating $R$ to $R \cup \set{\vtid}$ using an update rule for the authoritative set camera (in Line <ref>). As part of registering for helping, it first establishes $\linpending(\cssOp, k, v_p, T_0, \Phi)$ by transferring its obligation to linearize to the shared state, captured by the update token $\atomicUpdate(\Phi)$. The condition $\pastlin(\cssOp, k, v_p, T_0)$ follows from the fact that $\dSpec{op}(k, \abs{H_0(T_0)}, \abs{H_0(T_0)}, v_p)$ does not hold. The thread also creates a fresh non-duplicable token $\token$ that it will later trade in for the receipt $\Phi(v_p)$.

We are now at the point of invocation for $\cssOp$. Before continuing further, let us briefly switch to the role played by the concurrent thread that must linearize thread $\tid$. The helping thread must update the structure, and as per the invariant, update the history $M$ as well as the helping protocol $\helpinginv(H,T)$. In particular, while updating the helping protocol, it scans over all threads registered for helping so far, moving them from state $\linpending$ to state $\lindone$ as per the prophesied return value $v_p$.

Let us now return to the proof thread $\vtid$ at Line <ref>. As precondition of $(\ref{eq:hindsight-spec})$, we give away $\proph(p, \vpvs)$ and obtain the postcondition (Line <ref>). Simplifying the postcondition of $(\ref{eq:hindsight-spec})$ for our case $\neg \procProph(\vpvs)$, we obtain the predicate $\pastlin(\cssOp, k, v_p, T_0)$.
Next, we make a final resolution of the prophecy on Line <ref>. Since, $\vpvss$ is the suffix of $\vpvs$, $\prophend{v_p}$ must also be the final item in $\vpvss$. After resolution, we obtain $\prophend{v_p} = \prophend{v}$ and by injectivity of the end marker, $v_p = v$.

We now have the predicate $\pastlin(\cssOp, k, v, T_0)$ which we use to obtain the receipt of linearization from the shared invariant. Because $\pastlin(\cssOp, k, v, T_0)$ holds now, we know thread $\vtid$ cannot be in the $\linpending$ state. Hence, we know that thread $\vtid$ must be in the $\lindone$ state. Since the thread owns the unique token $\token$, it trades it in to obtain $\Phi(v)$, which lets it complete the proof of its client-level specification.

§ ADDITIONAL DETAIL ON VERIFICATION OF THE SKIPLIST TEMPLATE

§.§ Keysets Reasoning

Recall that keysets exhibit two properties that are crucial for localizing the functional correctness specification of search structures from the global data structure graph to individual nodes in the graph: (1) keysets partition the set of all keys, and (2) a node's contents is always a subset of its keyset. To capture these properties naturally in Iris, <cit.> introduces a keyset camera. An element of the keyset camera is a pair of sets of keys $(K, C)$ with $C \subseteq K$. We associate such pairs to regions in the data structure graph such that $C$ is the union of the node contents in the region and $K$ is the union of the nodes keysets. The composition of such pairs is defined as (pair-wise) disjoint union. The validity and the composition operator of the keyset camera then implicitly capture the desired properties (1) and (2) above.

Using this camera we tie the keyset reasoning to the invariant for the skiplist template by instantiating the predicate $\resourcesks$ (from <ref>) as follows:

\[\resourcesks(s) \defeq  \ghostState{}{\authAuth (\KS, C(s))} * \Sep_{n \in \fpof{s}} \ghostState{}{\authFrag (\keysetof{s, n}, \contentsof{s, n})}\enspace.\]

The assertion $\ghostState{}{\authAuth (\KS, C(s))}$ signifies ownership of the logical contents $C(s)$ of the structure in the state captured by snapshot $s$. Recall that $\KS$ is the set of all keys. The set $\fpof{s}$ tracks the footprint of $s$, i.e., the set of all nodes in the data structure graph captured by $s$. Each individual node $n \in \fpof{s}$ owns its keyset $\keysetof{s,n}$ and node-local logical contents $\contentsof{s,n}$. The keyset camera enforces that the $\keysetof{s,n}$ are pairwise disjoint, $\contentsof{s,n} \subseteq \keysetof{s,n}$ for each $n$, and that $C(s) = \bigcup_{n \in \fpof{s}} \contentsof{s,n}$, respectively,
$\keyspace = \bigcup_{n \in \fpof{s}} \keysetof{s,n}$.

A node's keyset and contents are then tied to the actual physical representation of the data structure via an abstract predicate that is instantiated for each node implementation. Recall that a node's keyset is defined in terms of its inset, an inductive quantity defined over the edgeset graph of the structure. As in <cit.>, we use the Flow Framework <cit.> to obtain a node-local characterization of the inset quantity and to reason about insets in Iris. We omit these details here as they are not relevant for understanding the high-level proof idea.

§.§ Helper Function Specifications

Our encoding of the hindsight specification $(\ref{eq:hindsight-spec})$ requires us to resolve a prophecy around each program step that may modify the structure. In the context of the skiplist template, the structure is modified using calls to the helper functions markNode and changeNext on the base-level list.
Unfortunately, prophecies in Iris can only be resolved around physical computation steps in the Iris programming language HeapLang and not at a more abstract level around logical atomic triples. Hence, the atomic triples for markNode and changeNext themselves must capture the relevant aspects of the reasoning related to prophecy resolution.

<Ref> shows these atomic triple specifications.

We focus on the markNode specification in particular. The assertions in blue are those already described in <ref>. The additional assertions in brown are concerned with the prophecy reasoning. The precondition $\prophcolor{\proph(p, \vpvs)}$ gives the right to resolve the prophecy $p$. The additional postcondition says that marknode resolves the prophecy an arbitrary number of times, but if it succeeds, then a Success value was seen in the list of prophesied values $\vpvs$, yielding $\procProph(\vpvs)$. Otherwise, it says that no Success value was seen so far, yielding $\procProph(\vprf)$. The template proof for delete then uses this information to infer whether $\procProph(\vpvs)$ holds and prove the appropriate postcondition from the hindsight specification. The specification of changeNext is similar.

$\annotAtom{k\,h\,\vmark\,\vnext.\; \nodeInv(n, k, h, \vmark, \vnext) * (0 < h) \prophcolor{* \proph(p, \vpvs)}}$
|<markNode>| $0$ $n$ $p$
$\annotAtom{\Ret x.\; \nodeInv(n, k, h, \vmarkp, \vnext) \prophcolor{* \proph(p, \vpvss) * (\vpvs = \vprf \;\code{++}\; \vpvss)}\\ * (\vmark(0) = \false \impl x = \mathsf{Success} * \vmarkp = \vmark[0 \rightarrowtail \true] \prophcolor{* \procProph(\vpvs)}) \\ * (\vmark(0) = \true \impl x = \mathsf{Failure} * \vmarkp = \vmark \prophcolor{* \neg \procProph(\vprf)})}$

$\annotAtom{k\,h\,\vmark\,\vnext.\; \nodeInv(n, k, h, \vmark, \vnext) * (0 < h) \prophcolor{* \proph(p, \vpvs)}}$
|<changeNext>| $0$ $n$ $n'$ $e$ $p$
$\annotAtom{\Ret x.\; \nodeInv(n, k, h, \vmark, \vnextp) \prophcolor{* \proph(p, \vpvss) * (\vpvs = \vprf \;\code{++}\; \vpvss)} \\ * ((\vmark(0) = \false \land \vnext(0) = n') \impl x = \mathsf{Success} * \vmarkp = \vmark[0 \rightarrowtail \true] \prophcolor{* \procProph(\vpvs)}) \\ * ((\vmark(0) = \true \lor \vnext(0) \neq n') \impl x = \mathsf{Failure} * \vmarkp = \vmark \prophcolor{* \neg \procProph(\vprf)})}$

Specifications of the helper functions with the prophecies.

§.§ Proof outline of delete

In this section, we discuss the proof of code in more detail.
The proof outline is shown in <ref>. We want to show that delete satisfies $(\ref{eq:hindsight-spec})$. The precondition provides access to the invariant $\mainInv(r)$ and knowledge that the thread ID is $\vtid$ with start time $t_0$. Additionally, the precondition provides the conjunct $(\procProph(\vpvs) \magicwand \atomicUpdate(\Phi))$, signifying that the thread can perform its linearization in case of a successful decisive operation. The precondition also provides the right to resolve prophecies. It is easy to see how prophecies are mainpulated by the helper functions from the specifications in <ref>, hence we ignore them in the proof outline.

The algorithm of delete begins with a call to traverse. The specification for traverse provides the postcondition

\[ \pastt{s, t_0}(k \in \keysetof{s, \vcurr} \land (\vres \iff k \in \contentsof{s, \vcurr})).\]

Note that we use the past operator $\pastt{s, t_0}$ from <ref> in the postcondition of traverse. Intuitively, this assertion captures that there is a past state $s$ in the history (after time point $t_0$) in which $k$ is in the keyset of $\vcurr$ and $\vres$ is true iff $k$ is in the logical contents of $\vcurr$. Note that this implies $\markof{s, \vcurr, 0} = \false$ due to Invariant <ref>.

The delete algorithm proceeds by case analysis on the result of traverse. Let us first consider the case that $\vres$ is $\false$ (Line <ref>). The delete operation terminates with result $\false$. The specification (<ref>) requires establishing the predicate $\pastlin(\code{del}, k, \false, t_0)$ in this case. To this end, we must provide a witness past state in which $k$ was not part of the abstract state. We obtain this witness from the postcondition of traverse which provides a past state $s$ such that $k \in \keysetof{s, c}$ and $k \notin \contentsof{s ,c}$. Applying (<ref>) in state $s$, we can establish the predicate $\pastlin(\code{del}, k, \false, t_0)$ (Line <ref>).

Let us now consider the case when $\vres$ is $\true$. The delete algorithm here calls the helper function maintainanceOp_del, which marks node $\vcurr$ at the higher levels. Thus, after maintainanceOp_del terminates, we obtain the information that all higher levels of $\vcurr$ are marked (Line <ref>). Next, the helper function markNode is called at the base level to logically delete $\vcurr$ from the structure. In order to apply the specification of markNode, we open the invariant $\mainInv(r)$ to access the $\nodeInv$ predicate for $\vcurr$ (Line <ref>). Let the current snapshot at this point (obtained by opening the invariant) be $s_0$. The call to markNode call either succeeds or fails depending on whether $\markof{s_0, \vcurr, 0} = \false$ holds. We consider both of the cases in turn.

First, suppose that markNode succeeds (Line <ref>). This implies that $\markof{s_0, \vcurr, 0} = \false$ and a new snapshot $s_1$ must be constructed to record the marking of $\vcurr$. The proof then appends $s_1$ to the history stored in $\mainInv(r)$ in order to reestablish $\mainInv(r)$. Additionally, success of markNode implies that $\procProph(\vpvs)$ holds. Hence, the thread must use the resource $\atomicUpdate(\Phi)$ to linearize itself. The receipt of linearization $\Phi$ is exactly what is required in the postcondition of (<ref>) in this case (Line <ref>).

Finally, consider the case that markNode fails (Line <ref>). The delete algorithm terminates with result $\false$ in this case. Hence, we must again establish $\pastlin(\code{del}, k, \false, t_0)$ to complete the proof. That is, we must identify a witness past state such that $k$ was not part of the abstract state of the structure. To compute this witness, note that $\markof{s, \vcurr, 0} = false$ for state $s$ observed by traverse, while $\markof{s_0, \vcurr, 0} = \true$ for the current state $s_0$. By $\transinv$ in <ref> and temporal interpolation, there must exist consecutive states $s_1$ and $s_2$ when $\vcurr$ was marked at the base level (Line <ref>). Here, the predicate $\paststate(s, t)$ represents the knowledge that the history recorded snapshot $s$ at time $t$. The snapshot $s_2$ is the required witness to establish the postcondition of $(\ref{eq:hindsight-spec})$ (Line <ref>). This completes the proof of delete.

[aboveskip=1pt,belowskip=0pt, frame=none]
$\annot{\minvr * \thread(\vtid, t_0) * (\procProph(\vpvs) \magicwand \atomicUpdate(\Phi))}$
let delete $k$ =
let $\vparr$ = allocArr $\vL$ $\vhead$ in
let $\vsarr$ = allocArr $\vL$ $\vtail$ in
let $\vpred$, $\vcurr$, $\vres$ = traverse $\vparr$ $\vsarr$ $k$ in@@
$\annot{\pastt{s, t_0}(k \in \keysetof{s, \vcurr} \land (\vres \iff k \in \contentsof{s, \vcurr}))}$
if not $\vres$ then
$\annot{\pastt{s, t_0}(k \in \keysetof{s, \vcurr} \land (k \notin \contentsof{s, \vcurr}))}$@@
$\annot{\pastt{s, t_0}(k \notin \abs{s})}$
$\annot{\pastt{s, t_0}(\dSpec{del}(k, \abs{s}, \abs{s}, \false))}$
$\annot{\neg \procProph(pvs) * \pastlin(\code{del}, k, \false, t_0)}$ @@
$\annot{\pastt{s, t_0}(k \in \keysetof{s, \vcurr} \land (k \in \contentsof{s, \vcurr}))}$
maintainanceOp_del $\vcurr$;
$\annot{\pastt{s, t_0}(\markof{s, \vcurr, 0} = \false) * \pastt{s', t_0}(\forall i, 0 < i < \htof{s', \vcurr} \impl \markof{s', \vcurr, i} = \true)}$@@
$\annot{\pastt{s, t_0}(\markof{s, \vcurr, 0} = \false) * \historyinv(H_0, T_0) * \resources(s_0) * \cdots}$
$\annot{\pastt{s, t_0}(\markof{s, \vcurr, 0} = \false) * \historyinv(H_0, T_0) * \nodeInv(\vcurr, s_0) * \cdots}$@@
match |<markNode>| 0 $\vcurr$ with
| Success ->
$\annot{(\markof{s_0, \vcurr, 0} = \false) * (\markof{s_1, \vcurr, 0} = \true) * \procProph(\vpvs) * \cdots}$@@
$\annot{\procProph(\vpvs) * \atomicUpdate(\Phi) * \dSpec{del}(k, \abs{s_0}, \abs{s_1}, \true) * \cdots}$
$\annot{\procProph(\vpvs) * \Phi * \historyinv(H_0[T_0+1 \rightarrowtail s_1], T_0+1) * \resources(s_1) * \cdots}$
traverse $\vparr$ $\vsarr$ $k$; $\true$
$\annot{\procProph(\vpvs) * \Phi}$@@
| Failure ->
$\annot{\pastt{s, t_0}(\markof{s, \vcurr, 0} = \false) * (\markof{s_0, \vcurr, 0} = \true) * \cdots}$@@
$\annot{(\exists\; s_1\; s_2\; t,\; (t_0 \leq t) * \paststate(s_1, t) * \paststate(s_2, t+1) * (\markof{s_1, \vcurr, 0} = \false) * (\markof{s_2, \vcurr, 0} = \true)) \cdots }$@@
$\annot{(t_0 \leq t) * \paststate(s_1, t) * \paststate(s_2, t+1) * (\keyof{s_2, c} \notin \abs{s_2}) \cdots }$
$\annot{\pastt{s_2, t_0}(\dSpec{del}(k, \abs{s_2}, \abs{s_2}, \false)) \cdots }$
$\annot{\neg \procProph(pvs) * \pastlin(\code{del}, k, \false, t_0)}$@@

Outline for the proof of the $\code{delete}$.


#  Unified Model of Temperature Dependence of Core Losses in Soft Magnetic
Materials Exposed to Nonsinusoidal Flux Waveforms and DC Bias Condition

Adam Ruszczyk<EMAIL_ADDRESS>ABB Corporate Research, Starowiślna
13a, 31-038 Kraków, Poland,  Krzysztof Sokalski<EMAIL_ADDRESS>Institute of Computer Science, Czȩstochowa University of Technology, Al. Armii
Krajowej 17, 42-200 Czȩstochowa, Poland

###### Abstract

Assuming that Soft Magnetic Material is a Complex System and expressing this
feature by scaling invariance of the power loss characteristic, the unified
model of the temperature dependence of Core Losses in Soft Magnetic Materials
Exposed to Nonsinusoidal Flux Waveforms and DC Bias Condition has been
constructed. In order to verify this achievement the appropriate measurement
data concerning power losses and the all independent variables have been
collected. The model parameters have been estimated and the power losses
modeling has been performed. Comparison of the experimental values of power
losses with their calculated values has showed good agreement.

###### pacs:

75.50.-y, 61.85.+p

The following article has been submitted to Applied Physics Letters. If it is
published, it will be found online at http://apl.aip.org

## Introduction

Application of soft magnetic materials in electronic devices requires
knowledge about losses under different conditions of exposition: sinusoidal
and nonsinusoidal flux waveforms of different shapes, with and without DC bias
condition. During the two last decades the two classes of core loss’ models
have been elaborated. The first class consists of models which are based on
the Steinmetz Equation (bib:Steinmetz, ), (bib:Albach, ), (bib:Reinert, ),
(bib:Li, ),(bib:Venka, ), (bib:Boss1, ), (bib:Ecklebe, ), (bib:Ecklebe1,
),(bib:FFio, ). However the second class is based on the assumption that the
shape of the waveform does not matter and as a result only look at peaks
(bib:Sokal1, ),(bib:Sokal2, ),(bib:Sokal3, ),(bib:Ruszcz, ) and (bib:Cale, ).
Non of them presents satisfactory algoritm enabling us to calculate of core
losses v.s. temperature of sample with and without presence of conditions for
exposition mentioned above. Therefore, this paper is devoted to solution of
this problem.

##  I Scaling and Unified Core Loss Model

On the base of our recent papers (bib:Sokal1, ),(bib:Ruszcz, ) we derive the
unified model of the total core loss versus the four independent variables:
$f$-frequency, $\triangle B$-pik to pik magnetic induction, $H_{DC}$-DC bias
and $T$-temperature:

$P_{tot}=F(f,\triangle B,H_{DC},T).$ (1)

In order to apply scaling to (1) the right hand side has to be homogeneous
function in general sense. This assumption has to be satisfied both, by the
experimental data and by the mathematical model. However, according to results
of researches presented in (bib:ABB1, ), (1) and measurement data formed by
the action of DC-bias are not uniform in the required sense. This problem we
have solved in the previous paper (bib:Ruszcz, ) by using the method invented
by Van den Bossche et al. (bib:Boss1, ). They have mapped the DC-bias into
primary magnetization curve. Using their idea we have used the following
mapping:

$H_{DC}\rightarrow[M_{0},M_{1},M_{2},M_{3}],$ (2)

where $M_{i}=tanh{(H_{DC}\cdot c_{i})}$ and $c_{i}$ are free parameters to be
determined from the experimental data. The number of $M_{i}$ components is
optional. The introduced mapping (2) enables us to write down the following
condition for $P_{tot}(f,\triangle B,[M_{0},M_{1},M_{2},M_{3}],T)$ to be a
homogenous function in general sense:

$\displaystyle\exists\\{a,b,c,d,g\\}\in{\bf
R^{5}}:\forall\lambda\in\bf{R_{+}}$ $\displaystyle
P_{tot}(\lambda^{a}f,\lambda^{b}(\triangle
B),\lambda^{c}[M_{0},M_{1},M_{2},M_{3}],\lambda^{d}T)=$
$\displaystyle\lambda^{g}P_{tot}(f,\triangle B,[M_{0},M_{1},M_{2},M_{3}],T).$
(3)

Substituting for $\lambda$ the following expression:
$\lambda=(\triangle B)^{-1/b}$ we derive the most general form for $P_{tot}$
which satisfies (3):

$P_{tot}=(\triangle B)^{\beta}\,F\left(\frac{f}{(\triangle
B)^{\alpha}},\frac{[M_{0},M_{1},M_{2},M_{3}]}{(\triangle
B)^{\gamma}},\frac{T}{(\triangle B)^{\delta}}\right),$ (4)

where,
$\alpha=\frac{a}{b},\beta=\frac{g}{b},\gamma=\frac{c}{b},\delta=\frac{d}{b}$
and $F(\cdot,\cdot,\cdot)$ is an arbitrary function to be determined.

##  II The modeling of $F(\cdot,\cdot,\cdot)$

In order to determine $F(\cdot,\cdot,\cdot)$ we assume its form to be
factorable:

$\displaystyle F\left(\frac{f}{(\triangle
B)^{\alpha}},\frac{[M_{0},M_{1},M_{2},M_{3}]}{(\triangle
B)^{\gamma}},\frac{T}{(\triangle B)^{\delta}}\right)=$
$\displaystyle\Phi\left(\frac{f}{(\triangle
B)^{\alpha}},\frac{[M_{0},M_{1},M_{2},M_{3}]}{(\triangle
B)^{\gamma}}\right)\,\Theta\left(\frac{T}{(\triangle B)^{\delta}}\right).$ (5)

$\Phi(\cdot,\cdot)$ is a version of very well working model function derived
in (bib:Ruszcz, ):

$\displaystyle\Phi(\frac{f}{(\triangle
B)^{\alpha}},H_{DC})=\Sigma_{i=1}^{4}\Gamma_{i}\left(\frac{f}{(\triangle
B)^{\alpha}}\right)^{i\,(1-x)}+$
$\displaystyle\Sigma_{i=0}^{3}\Gamma_{i+5}\left(\frac{f}{(\triangle
B)^{\alpha}}\right)^{(i+y)(1-x)}\frac{tanh(H_{DC}\cdot c_{i})}{(\triangle
B)^{\delta}}.$ (6)

Basing on some computer experiments we have selected for $\Theta(\cdot)$ the
following Padé approximant (bib:pade, ):

$\Theta=\left(\frac{\psi_{0}+\theta\,(\psi_{1}+\theta\,\psi_{2})}{1+\theta\,(\psi_{3}+\theta\,\psi_{4})}\right)^{1-z},$
(7)

where $\theta=\frac{T+\tau}{\Delta B^{\gamma}}$, $T^{\circ}C$ is measured
temperature, $\tau$ and $z$ are tuning parameters, $\psi_{i}$ are Padé
expansion coefficients.

##  III Experimental Data, Estimations of Parametr’s and Modeling

Table 1: Selected 60 records of the measurement data of SIFERRIT N87  $T[^{o}C]$ | $\triangle B[T]$ | $f[kHz]$ | $H_{DC}[\frac{A}{m}]$ | $P_{tot}[\frac{W}{m^{3}}]$ | $T[^{o}C]$ | $\triangle B[T]$ | $f[kHz]$ | $H_{DC}[\frac{A}{m}]$ | $P_{tot}[\frac{W}{m^{3}}]$
---|---|---|---|---|---|---|---|---|---
28,1 | 0,395 | 1 | 8,634 | 4064,3 | 28,1 | 0,391 | 1 | 20,146 | 4469,0
28,1 | 0,374 | 1 | 60,634 | 6332,4 | 28,3 | 0,351 | 1 | 86,651 | 6463,6
17,7 | 0,398 | 2 | 7,8014 | 9452,1 | 17,8 | 0,398 | 2 | 20,555 | 10663,8
18,9 | 0,396 | 2 | 35,583 | 12745,8 | 18,5 | 0,377 | 2 | 89,240 | 16015,6
26,2 | 0,400 | 5 | 6,570 | 21131,3 | 26,4 | 0,400 | 5 | 17,820 | 23110,0
26,5 | 0,398 | 5 | 33,230 | 28057,3 | 27,1 | 0,386 | 5 | 89,400 | 35209,8
28,4 | 0,401 | 10 | 5,892 | 41549,0 | 28,6 | 0,401 | 10 | 17,477 | 45257,9
28,8 | 0,400 | 10 | 31,820 | 54650,9 | 29,7 | 0,393 | 10 | 73,960 | 63821,6
30,8 | 0,386 | 10 | 105,00 | 64632,1 | 28,4 | 0,490 | 1 | 11,694 | 6611,0
28,4 | 0,488 | 1 | 24,299 | 7196,0 | 28,4 | 0,451 | 1 | 78,390 | 8771,6
19,1 | 0,497 | 2 | 10,120 | 15234,1 | 19,2 | 0,496 | 2 | 23,718 | 16781,0
19,3 | 0,485 | 2 | 54,63 | 19235,9 | 19,8 | 0,475 | 2 | 76,86 | 20100,2
27,7 | 0,502 | 5 | 8,92 | 34634,8 | 27,4 | 0,503 | 5 | 15,02 | 36195,2
27,7 | 0,501 | 5 | 21,5 | 37496,6 | 28,6 | 0,496 | 5 | 47,5 | 41259,7
31,7 | 0,499 | 10 | 20,52 | 71226,8 | 32,15 | 0,494 | 10 | 45,04 | 76876,5
32,6 | 0,487 | 10 | 67,14 | 80858,2 | 28,5 | 0,588 | 1 | 14,42 | 10042,9
28,7 | 0,561 | 1 | 57,97 | 11239,6 | 28,7 | 0,541 | 1 | 78,08 | 11255,7
29,1 | 0,58 | 2 | 12,82 | 19689,9 | 28,7 | 0,576 | 2 | 54,36 | 22043,0
30,1 | 0,592 | 5 | 42,4 | 52126,7 | 31,1 | 0,599 | 10 | 10,29 | 92648,6
31,3 | 0,595 | 10 | 31,23 | 96446,4 | 28,9 | 0,684 | 1 | 22,05 | 14150,5
28,1 | 0,389 | 1 | 33,507 | 5358,8 | 28,4 | 0,346 | 1 | 91,066 | 6376,4
18,2 | 0,386 | 2 | 68,034 | 15049,1 | 18,7 | 0,367 | 2 | 110,59 | 16027,7
29 | 0,669 | 1 | 41,33 | 14417,5 | 34,7 | 0,586 | 10 | 61,25 | 96583,3
30,2 | 0,616 | 5 | 36,05 | 54344,9 | 28,7 | 0,586 | 2 | 33,49 | 21002,2
28,5 | 0,580 | 1 | 36,01 | 10790,0 | 42,1 | 0,496 | 50 | 47,53 | 289491,2
31,5 | 0,499 | 10 | 7,57 | 65879,7 | 28,1 | 0,500 | 5 | 31,42 | 39530,2
20,2 | 0,469 | 2 | 87,44 | 20547,5 | 19,7 | 0,480 | 2 | 68,36 | 20073,3
28,5 | 0,443 | 1 | 85,100 | 8702,4 | 28,3 | 0,473 | 1 | 54,300 | 8296,5
30,2 | 0,387 | 10 | 99,190 | 64410,1 | 29,2 | 0,396 | 10 | 61,172 | 62814,4
27,5 | 0,386 | 5 | 97,779 | 35945,6 | 26,8 | 0,394 | 5 | 58,800 | 32614,3
Figure 1:  Projection of the measurement points and the scaling theory points
(5)-(7) in $[f/(\triangle B^{\alpha})^{(1-x)},P_{tot}/(\triangle B^{\beta})]$
plane. Figure 2:  Projection of the measurement points and the scaling theory
points (5)-(7) in $[tanh(H\,c_{1},P_{tot}/(\triangle B)^{\beta}]$ plane.

The B-H Loop measurements have been performed for SIFERRIT N87. The Core
Losses per unit volume have been calculated as the enclosed area of the B-H
loop, multiplied by the frequency f. The following factors influence the
accuracy of measurements: 1) Phase Shift Error of Voltage and Current $<4\%$,
2) Equipment Accuracy $<5,6\%$, 3) Capacitive Couplings negligible (capacitive
currents are relatively lower compared to inductive currents), and 4)
Temperature $<4\%$. For details of the applied measurement method and the
errors of the relevant factors we refer to (bib:Ecklebe, ), (bib:Ecklebe1, ).
The parameter values of (4)-(7) have been estimated by minimization of
$\chi^{2}$ using the Simplex method of Nelder and Mead (bib:pade, ) and the
our experimental data. The measurement series consists of $60$ points, see
TABLE 1. Standard deviation per point is equal to
$15[\frac{W}{m^{3}T^{\beta}}]$ Applying the formulae (4)-(7) and the estimated
parameter values TABLE 2 we have drawn the three scatter plots Fig. 1, Fig. 2
and Fig. 3, which compare estimated points with the experimental ones in the
three projections, respectively. Note that, in order to prevent generation of
large numbers in the estimation process the unit of frequency was kHz while
other magnitudes were expressed in SI unit system.

Table 2: The set of estimated model’s parameters of (4)-(7) for $\delta=0$ $\alpha$ | $\beta$ | $x$ | $\Gamma_{1}$ | $\Gamma_{2}$ | $\Gamma_{3}$ | $\Gamma_{4}$ | $\Gamma_{5}$
---|---|---|---|---|---|---|---
${\small-11,628}$ | -8,6382 | 0,52629 | -1,4083 | 739,55 | 1253,4 | 4238,5 | 0,12264
$\Gamma_{6}$ | $\Gamma_{7}$ | $\Gamma_{8}$ | y | $\psi_{3}$ | $c_{3}$ | $\psi_{4}$ | $\psi_{5}$
-30,972 | -51,869 | -4201,45 | 0,28877 | 14,4558 | 0,1648 | -1,27E-01 | 0,28302
$c_{2}$ | $\tau$ | $\gamma$ | $\psi_{2}$ | $\psi_{1}$ | $c_{1}$ | $c_{0}$ | z
-0,1808 | 7,77E-02 | -0,17954 | 2,3966 | -0,8993 | -2,44E-02 | -0,4877 | 4,84E-02
Figure 3:  Projection of the measurement points and the scaling theory points
(5)-(7) in $[\frac{T+\tau}{(\triangle B)^{\gamma}},P_{tot}/(\triangle
B)^{\beta}]$ plane.

##  IV Conclusions

Efficiency of the scaling in solving problems concerning of power losses in
Soft Magnetic Materials has been confirmed all ready in the recent papers
(bib:Sokal1, )-(bib:Ruszcz, ). However, this paper is the first one which
presents application of scaling in modeling of temperature dependence of the
core loss. The presented method is universal, which means that it works for
wide spectrum of expositions and different soft magnetic materials. Moreover
the presented model formulae (4)-(7) are not closed and can be adapted for a
current problem by fitting the forms of both factors $\Phi$ and $\Theta$. At
the end one must say that success in applying the scaling depends on property
of data. The data must obey the scaling.

##

## References

  * (1) C.P. Steinmetz, On the law of hysteresis, Trans. Amer. Inst. Elect. Eng., 9, 3-64 (1892).
  * (2) M. Albach, T. Durbaum, and A. Brockmeyer, IEEE Power Electronics Specialists Conference, pp. 1463 1468 (1996).
  * (3) J. Reinert, A. Brockmeyer J. Reinert, A. Brockmeyer, and R.W. De Doncker, Calculation of losses in ferro- and ferrimagnetic materials based on the modified Steinmetz equation, Annual Meeting of the IEEE Industry Applications Society, 1999.
  * (4) Jieli Li, T. Abdallah, and C. R. Sullivan, Improved calculation of core loss with nonsinusoidal waveforms, in Annual Meeting of the IEEE Industry Applications Society, 2001, pp. 2203-2210.
  * (5) K. Venkatachalam, C. R. Sullivan, T. Abdallah, and H. Tacca, Accurate prediction of ferrite core loss with nonsinusoidal waveforms using only Steinmetz parameters IEEE Workshop on Computers in Power Electronics (COMPEL), 2002.
  * (6) Alex Van den Bossche, Vencislav Valchev, Georgi Georgiev, Measurement and loss model of ferrites in nonsinusoidal waves, IEEE Power Electronics Specialists Conference, 2004.
  * (7) Jonas Mühlethaler, Jürgen Biela, Johann Walter Kolar and Andreas Ecklebe, Core-Loss Calculation for Magnetic Components Employed in Power Electronic Systems, IEEE TRANSACTIONS ON POWER ELECTRONICS, 27, pp.964-973 (2012).
  * (8) J. Mühlethaler, J. Biela, J.W. Kolar, A. Ecklebe, Core Losses Under the DC Bias Condition Based on Steinmetz Parameters, IEEE Transactions on Power Electronics, 27, pp.953-963 (2012).
  * (9) F. Fiorillo and A. Novikov, An improved approach to power lossess in magnetic laminations under nonsinusoidal induction waveform, IEEE Trans. Magnet., 26, pp.2559-2561 (1990).
  * (10) K. Sokalski, J. Szczyg owski, M. Najgebauer and W. Wilczy nski, Thermodynamical Scaling of Eddy Current Losses in Magnetic Materials, Proc. 12th IGTE Symposium, 2006.
  * (11) K. Sokalski, J. Szczygłowski, M. Najgebauer and W. Wilczyński, [12] K. Sokalski, J. Szczyg owski, M. Najgebauer and W. Wilczy nski, Losses scaling in soft magnetic materials, COMPEL: Int. J. Comput. Math. Electr. Electron. Eng.,26, 640-649 ( 2007), COMPEL: Int. J. Comput. Math. Electr. Electron. Eng.,26, 640-649 ( 2007).
  * (12) K. Sokalski, J. Szczyg owski, and W. Wilczy nski, Scaling conception of power loss separation in soft magnetic materials, http://arxiv.org/abs/1111.0939v1.
  * (13) A. Ruszczyk, K. Sokalski, J. Szczygłowski, Scaling in Modeling of Core Losses in Soft Magnetic Materials Exposed to Nonsinusoidal Flux Waveforms and DC Bias, SMM21 Conference, Budapest 2013.
  * (14) J. Cale, S.D. Sudhoff, S. D. and R.R. Chan, A Field-Extrema Hysteresis Loss Model for High-Frequency Ferrimagnetic Materials, IEEE Transactions on Magnetics, vol. 44, issue 7, pp. 1728-1736 (2008).
  * (15) K. Sokalski, J. Szczygłowski, ABB REPORT, PLCRC/50002437/02/1725/2011.
  * (16) William H. Press, Saul A. Teukolsky, William T. Vetterling, Brian P. Flannery, Numerical Recipes in Fortran 77, The Art of Scientific Computing, Second Edition, Volume 1 of Fortran Numerical Recipes, Published by the Press Syndicate of the University of Cambridge 1997, p. 194.