The rule rel-wp-l says that we can “take out” an expression $\expr_1$ in context $\lctx$ on the left-hand side, and reason about it using Iris's weakest precondition.
The rule rel-wp-atomic-l is similar, but it also allows for opening an invariant around $\expr_1$, in case $\expr_1$ is atomic.[Iris's weakest precondition connective $\wpre \expr [\mask] \pred$ is also equipped with a mask to keep track of which invariants may be opened.
This was the inspiration for the mask annotation at 's refinement judgment.]
The rule rel-step-r says that if we have an expression $\expr_2$ on the right-hand side in an evaluation context $\lctx$, and we can reduce $\expr_2$ to a value $\val_2$, using the ghost thread pool rules,
then we can reduce the refinement proposition to $\logrel[\mask]{}{\expr_1}{\fillctx\lctx[\val_2]}{\type}$.

§.§ Soundness

Utilizing the definitions in this section, we outline the proof of the soundness theorem (<Ref>), which says that 's refinement judgment is sound contextual refinement.
Formally, if $\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}$ is derivable in for any $\Delta$ with $\tenv \subseteq \dom(\Delta)$, then $\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}$.
To prove this theorem we make use of two key lemmas: adequacy of the refinement judgment (<Ref>), and the fact that the refinement judgment is a precongruence (<Ref>).

If $\proves \logrel{\Delta}{\expr_1}{\expr_2}{\type}$ is derivable in ,
and $(\expr_1, \stateS) \tpstep^{\ast} (\conS{\val_1}\efs_1, \stateS'_1)$,
then there exists $\val_2, \efs_2$, and $\stateS'_2$ such that
$(\expr_2, \stateS) \tpstep^{\ast} (\conS{\val_2}{\efs_2}, \stateS'_2)$.

Let $\pctx$ be a well-typed context
$\typedctx{\pctx}{\tenv}{\vctx}{\type}{\tenv'}{\vctx'}{\type'}$, then we have

\[
\always (\All \Delta. \logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type})
\wand (\All \Delta'. \logrel{\Delta'}[\vctx']{\fillctx\pctx[\expr_1]}{\fillctx\pctx[\expr_2]}{\type'})
\]

where $\Delta$ and $\Delta'$ contain at least the type variables in $\tenv$ and $\tenv'$, respectively.

<Ref> is proved by induction on $\pctx$ making using of 's type-directed structural rules (<Ref>).
The proof of <Ref> is rather involved, so before we discuss that, let us see how we prove the soundness theorem by putting these two lemmas together.

Let $\tenv$ be a type environment, and suppose that $\logrel{\Delta}[\vctx]{\expr_1}{\expr_2}{\type}$ is derivable in for any $\Delta$ with $\tenv \subseteq \dom(\Delta)$.
To prove $\ctxref{\tenv \mid \vctx}{\expr_1}{\expr_2}{\type}$,
suppose we have typed context $\typedctx{\pctx}{\tenv}{\vctx}{\type}{\emptyset}{\emptyset}{\type'}$,
and reduction $(\fillctx\pctx[\expr_1], \emptyset) \tpstep^{\ast} (\conS{\val_1}{\efs_1}, \stateS_1)$.
By <Ref>, we have
\logrel{}{\fillctx\pctx[\expr_1]}{\fillctx\pctx[\expr_2]}{\type'}
Then, by <Ref>, we get that $(\fillctx\pctx[\expr_2], \emptyset) \tpstep^{\ast} (\conS{\val_2}{\efs_2}, \stateS_2)$ for some $\val_2, \efs_2$ and $\stateS_2$, which concludes the proof.

Suppose that $\logrel{\Delta}{\expr_1}{\expr_2}{\type}$ is derivable in , and we have $(\expr_1, \stateS) \tpstep^{\ast} (\conS{\val_1}\efs_1, \stateS'_1)$.
Now we should exhibit $\val_2, \efs_2$, and $\stateS'_2$ such that $(\expr_2, \stateS) \tpstep^{\ast} (\conS{\val_2}{\efs_2}, \stateS'_2)$.
The high-level structure of the proof is as follows.
First, we allocate the thread pool invariant $\specctx$ and $0 \tpto \expr_2$ for the main-thread of the right-hand side.
Second, by definition of the refinement judgment, we obtain a weakest precondition $\wpre{\expr_1}{\Ret \val_1. \Exists \val_2. 0 \tpto \val_2 \ast \Sem{\type}_{\Delta}(\val_1, \val_2)}$.
Third, by opening $\specctx$ and using adequacy of Iris's weakest preconditions, we obtain $(\expr_2, \stateS) \tpstep^{\ast} (\conS{\val_2}{\efs_2}, \stateS'_2)$.

Carrying out these steps in detail—notably, setting up the required ghost theory for the ghost thread pool—involves some intricate reasoning using Iris features that are out of scope for this paper.
We thus refer the interested reader to the Coq mechanization, and only highlight the key part—the definition of the thread pool invariant $\specctx$:

\[
\specctx \eqdef \Exists \vec\expr_0,\stateS_0. \knowInv{\namesp_{\textnormal{\reloc}}}{
\Exists \vec{\expr},\stateS.
\specinv(\vec{\expr}, \stateS) \ast
(\vec{\expr}_0, \stateS_0) \tpstep^{\ast} (\vec{\expr}, \stateS)
\]

The invariant asserts that given an initial configuration $(\vec\expr_0,\stateS_0)$ for the right-hand side (which we set to be $(\expr_2,\stateS)$ when allocating the invariant), the configuration $(\vec{\expr}, \stateS)$ can be reached via the reduction $(\vec{\expr}_0, \stateS_0) \tpstep^{\ast} (\vec{\expr}, \stateS)$.
Here, $\specinv(\vec{\expr}, \stateS)$ is a connective defined using Iris's ghost theory that keeps track of the configuration of the ghost thread pool and ensures it is consistent with the $\tpto$ and $\mapstoS$ connectives.
The latter is essential, as it allows us to conclude from $\specinv(\vec{\expr}, \stateS)$ and $0 \tpto \val_2$ (as given by the post condition of the weakest precondition in the definition of the refinement judgment) that $\vec{\expr}$ is equal to $\conS{\val_2}{\efs_2}$ for some $\efs_2$.
By definition of the invariant $\specctx$, this gives us a reduction $(\expr_2, \stateS) \tpstep^{\ast} (\conS{\val_2}{\efs_2}, \stateS'_2)$ for the right-hand side, which is needed to conclude the third step of the proof.

§ THE COQ MECHANIZATION OF

The Coq mechanization of provides a soundness proof of and infrastructure to carry out interactive tactic-based refinement proofs.
It is built on top of the mechanization of Iris in Coq [54] and the Iris Proof Mode/MoSeL framework for tactic-based proofs in separation logic [68, 65].
In this section we examine the way 's language and type system are defined (<Ref>), and how the logic is defined on top of that (<Ref>).
We then describe 's tactic support for interactive refinement proofs, which allows us to seamlessly carry out proofs in Coq similar to those we have seen in this paper (<Ref>).
Finally, we give an overview of the source code (<Ref>).

§.§ The programming language

Iris is a programming language independent framework, which means that it can be instantiated with a programming language of choice.
In this paper, we do not make use of this generality, and use —the default language shipped with Iris's Coq development, which is essentially an untyped version of the language we considered in <Ref>.
is represented via a deep embedding and comes with a set of notations so that programs can be written in Coq-style syntax.
For example, the Boolean implementation $\bitbool$ of the bit module from <Ref> is written as follows:

Definition bit_bool : expr :=
(#true, (λ: "b",  "b"), (λ: "b", "b")).

Binders in are represented as strings, which makes it possible to write programs in a human-readable way.
This works well in practice because expression-level substitution only acts on closed terms, and thus does not need to be capture avoiding.

We equip with a type system in the usual way—types type are defined as an inductive data type, and the typing judgment typed is defined as an inductive relation:
Inductive type :=
| TVar : var → type
| TProd : type → type → type
| TArrow : type → type → type
| TExists : bind 1 of type → type
| (* ... *).
Inductive typed : stringmap type → expr → type → Prop :=
| Var_typed Γ x τ :
Γ !! x = Some τ → (Γ ⊢ₜ Var x : τ)
| Pair_typed Γ e1 e2 τ1 τ2 :
(Γ ⊢ₜ e1 : τ1) → (Γ ⊢ₜ e2 : τ2) → (Γ ⊢ₜ (e1, e2) : τ1 * τ2)
| Fst_typed Γ e τ1 τ2 :
(Γ ⊢ₜ e : τ1 * τ2) → (Γ ⊢ₜ Fst e : τ1)
| (* ... *).

We use the notation Γ ⊢ₜ e : τ for typed Γ e τ, and overload the standard Coq notations for types, we use the notation τ1 * τ2  for TProd τ1 τ2  and τ1 → τ2  for TArrow τ1 τ2 .
Since type-level substitution acts on (potentially) open terms, and therefore needs to be capture avoiding,
we use De Bruijn indices to represent type-level binders through the Autosubst Coq library [94].
For example, the type $\tbit \eqdef \texists{\tvar. \tvar \times (\tvar \to \tvar) \times (\tvar \to \tbool)}$ from <Ref> is represented in Coq as follows ( is notation for TVar):
Definition bitτ : type := ∃: #0 * (#0 → #0) * (#0 → TBool).

§.§ The logic

Recall from <Ref> that is defined as a shallow definition in Iris—the connectives are definitions in Iris, and the proof rules are lemmas in Iris.
In Coq we follow the same approach.
At the core of we have the definition lrel of semantic types, persistent Iris relations over values:
Record lrel Σ := LRel
lrel_car :> val → val → iProp Σ;
lrel_persistent v1 v2 : Persistent (lrel_car v1 v2)

Here, iProp Σ is the type of Iris propositions.[The parameter $\Sigma$ describes the kind of ghost state available in Iris.
It is an important but technical detail that can safely be ignored for the purpose of this paper.
An interested reader is directed to <cit.>.]
The record bundles together a relation together with a proof that it is persistent.
The notation :> declares the field lrel_car as a coercion.
In the Coq mechanization of we generalize the refinement judgment $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ to range over semantic types (lrel) instead of syntactic types (type):
Definition refines (E : coPset) (e1 e2 :$\,$expr) (A$\,$:$\,$lrel Σ) : iProp Σ :=
∀ j K, spec_ctx -∗ j ⤇ fill K e2 =E,⊤=∗
WP e1  v1, ∃ v2, j ⤇ fill K (of_val v2) ∗ A v1 v2 .

The parameter E corresponds to the mask $\mask$, and the semantic type A corresponds to the type interpretation $\Sem{\type}_{\Delta}$.
We use the notation REL e1 << e2 @ E : A for refines E e1 e2 A.
This definition makes use of the ghost thread pool connectives spec_ctx and j ⤇ e, as discussed in <Ref>, and which were originally defined in Coq in [68].

To formalize the refinement judgment on syntactic types, we first define the semantic interpretation $\Sem{\type}_{\Delta}$, denoted as interp τ Δ in Coq, which maps syntactic types $\type$ to semantic types.
To define the semantic interpretation, we define semantic type formers, which are combinators on semantic types corresponding to each syntactic type former.
For example, the semantic product type is defined as follows:
Definition lrel_prod (A B : lrel Σ) : lrel Σ := LRel (λ v1 v2,
∃ w1 w2 w1' w2', ⌜v1 = (w1,w1')

Here, we use Iris's notion ⌜φ⌝ to embed Coq propositions φ : Prop into Iris, although on paper we take the equality predicate to be primitive.
With the above definitions at hand, we can now define 's refinement judgment $\logrel[\mask]{\Delta}{\expr_1}{\expr_2}{\type}$ as REL e1 << e2 @ E : interp τ Δ .

The proof rules.
For example, the rule rel-load-r is formalized as the following lemma:
Lemma refines_load_r E K l q v e1 A :
↑ relocN ⊆ E →
l ↦ₛq v -∗
(l ↦ₛq v -∗ REL e1 << fill K (of_val v) @ E : A) -∗
REL e1 << fill K !#l @ E : A.

The lemma states that, under the assumption that $\namecl{\textlog{relocN}} \subseteq \mask$ ('s internal invariants are available in the mask $\mask$), the following separation logic formula holds:

\[
\loc \fmapstoS[q] \val \wand (\loc \fmapstoS[q] \val \wand{} \logrel[\mask]{}{\exprB}{\fillctx\lctx[\val]}{A})
\wand \logrel[\mask]{}{\exprB}{\fillctx\lctx[\deref \loc]}{A}
\]

This is exactly the internalization of rel-load-r.
The other proof rules are mechanized in a similar way.

The versions of 's soundness theorem for closed (<Ref>) and open terms (<Ref>) are stated in Coq as follows:
Lemma refines_sound Σ `relocPreG Σ e1 e2 τ :
(∀ `relocG Σ Δ, ⊢ REL e1 << e2 : interp τ Δ) →
∅ ⊨ e1 ≤ctx≤ e2 : τ.
Lemma refines_sound_open Σ `relocPreG Σ Γ e1 e2 τ :
(∀ `relocG Σ Δ, ⊢ Δ;Γ ⊨ e1 ≤log≤ e2 : τ) →
Γ ⊨ e1 ≤ctx≤ e2 : τ.

Here, Γ ⊨ e1 ≤ctx≤ e2 : τ is the notion of contextual refinement, Δ;Γ$\}$ ⊨  e1 ≤log≤ e2 : τ is the refinement judgment lifted to open expressions, and ⊢ P expresses that the Iris proposition P is derivable.

Example proof: refinement of the bit module.
In order to prove the contextual refinement ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitτ from <Ref>, it suffices to prove the following:
Lemma bit_refinement Δ : ⊢ REL bit_bool << bit_nat : interp bitτ Δ.

To prove this lemma, we use the relation R, which is the same as the one in <Ref>, but wrapped into a semantic type (lrel) to ensure it is persistent:
Definition R : lrel Σ := LRel (λ v1 v2,
(⌜v1 = #true⌝ ∧ ⌜v2 = #1⌝) ∨ (⌜v1 = #false⌝ ∧ ⌜v2 = #0⌝)).

Using the relation R, a Coq proof of the desired refinement is as follows:
Lemma bit_refinement Δ : ⊢ REL bit_bool << bit_nat : interp bitτ Δ.
unfold bitτ; simpl. iApply (refines_exists R). (* apply $\mbox{\ruleref{rel-pack}}$ *)
progress repeat iApply refines_pair. (* repeatedly apply $\mbox{\ruleref{rel-pair}}$ *)
- rel_values. (* apply $\mbox{\ruleref{rel-return}}$ and solve the goal *)
- (* ... *)

Finally, we combine bit_refinement with the soundness theorem to get a closed proof of contextual refinement:
Theorem bit_ctx_refinement : ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitτ
Proof. auto using (refines_sound relocΣ), bit_refinement. Qed.

It is important to emphasize that the contextual refinements, which we obtain in theorems like bit_ctx_refinement above, are closed propositions in Coq.
The statement (the type) of bit_ctx_refinement does not refer to or Iris.
This illustrates that the only parts of the trusted code base of our development are the notions that are involved in the definition of contextual refinement, the operational semantics and the typing of contexts.

§.§ Tactic support for interactive proofs

To prove refinement judgments, like the bit refinement REL bit_bool << bit_nat : interp bitτ Δ from the previous section, we can repeatedly apply the Iris lemmas corresponding to the proof rules.
However, doing so directly quickly becomes unwieldy, as the user has to manually provide the resources (like the precondition l ↦ₛq$\}$ v of refines_load_r), and manually select the evaluation context K.
For better usability we provide tactic support for symbolic execution.

Interactive separation logic proofs.
To explain the tactics for that we have defined, let us first look at the general tactic support in Iris.
The Iris Proof Mode (IPM) [68] and its successor MoSeL [65] allow us to carry out separation logic proofs interactively, in the style of regular tactic-based proofs in Coq.

P -∗ (P -∗ Q) -∗ Q

Before executing any tactics.

"H1" : P
"H2" : P -∗ Q

After iIntros "H1 H2".

Interactive proof of lemma example in IPM.

IPM provides a convenient representation of sequents for separation logic and tactics for manipulating them, allowing for interactive proof development in the style of regular proofs in Coq.
To illustrate this, consider the following separation logic tautology:
Lemma example (P Q : iProp Σ) : P -∗ (P -∗ Q) -∗ Q.
Proof. iIntros "H1 H2". iApply ("H2" with "H1"). Qed.

The intermediate results can be seen in <Ref>.
Applying iIntros "H1 H2". introduces the hypothesis P and P -∗ Q into the IPM context, giving them names H1 and H2, respectively.
Then, iApply ("H2" with "H1"). applies the separating implication P -∗ Q to the goal, using the hypothesis H1 : P as the assumption.

Symbolic execution tactics.
In addition to tactics like iIntros and iApply, IPM provides tactic for symbolic execution in weakest preconditions.
We built similar tactics on top of IPM for symbolic execution in refinement judgments.
For example, consider:
Lemma example_load l : l ↦ₛ #0 -∗ REL #2 << (!#l + #2) : lrel_int.
Proof. iIntros "Hl". rel_load_r. rel_pures_r. rel_values. Qed.

"Hl" : l ↦ₛ #0
REL #2 << (!#l + #2) : lrel_int

Before applying rel_load_r.

"Hl" : l ↦ₛ #0
REL #2 << (#0 + #2) : lrel_int

After applying rel_load_r.

"Hl" : l ↦ₛ #0
REL #2 << #(0 + 2) : lrel_int

After applying rel_pures_r.

Interactive refinement proof of lemma example_load in .

The results of rel_load_r and rel_pures_r can be seen in <Ref>.
The tactic rel_load_r symbolically executes the dereferencing operation, and the tactic rel_pures_r symbolically executes as many pure reduction steps as possible.
The tactic rel_values finishes the goal since both sides are values.
Similarly, we built tactics for all other language connectives (both on the left- and right-hand side).
The tactics were developed in a similar way to the weakest-precondition tactics from IPM, and we refer the reader to [68] for details.

§.§ Overview of the source code.

The Coq mechanization contains around 10300 lines of code, of which approximately

* 1315 lines for mechanization of the model of (<Ref>), including the adequacy theorem (<Ref>), and the primitive and derived rules (<Ref>);

* 1200 lines for the tactics (<Ref>);

* 1450 lines for the mechanization of the type system (<Ref>), and the soundness theorem for open term (<Ref>);

* 6050 lines for the examples and case studies (including the case studies we describe in the upcoming <Ref>);

* and 140 lines for tests (mainly regression tests for the tactics).

§ RELATED WORK

We described some of the most closely related work in the introduction (<Ref>), we now
discuss other related work on logical relations models, relational logics, atomic specifications, speculative reasoning, and linearizability.

Logical relations models.
Logical relations models over denotational and operational semantics have an extensive history.
To cover advanced programming language features such as recursive types and higher-order references, logical relations with step-indexing have been introduced [1, 5, 4, 22].
Step-indexing has shown to be very effective by a large body of work on step-indexed logical relations models,  [77, 48, 23, 25, 87].
However, in these papers step-indices appear explicitly in the definition of the logical relations model and the proofs about it.
In contrast in this paper we have used the “logical approach” to step-indexed logical relations.
This approach, pioneered by Dreyer in the LSLR logic [28], hides step-indices by abstracting and internalizing them in a logic using the later modality ($\later$) [9].
Dreyer used this approach to construct a binary logical relations model for System F with recursive types [28], and later extended the approach as part of the LADR logic to cover existential types and references [34].

The logical approach to logical relations was further refined by Turon  [102, 97], culminating in the CaReSL logic, who showed
how Hoare triples and ghost thread pools can be used to define a binary logical relation for fine-grained concurrency.
Subsequently, a version of this binary logical relation was defined and mechanized in Iris by Krebbers  [68] and Timany [98].
However, in these papers, logical refinement judgments are meta-logical statements, and because of that, there are no high-level proof rules for establishing and combining refinements.
Instead, to prove a refinement judgment, the user of the logic had to unfold the definition of the refinement judgment, and reason directly in CaReSL or Iris.
In this work we provide a generalization that makes refinement judgments first-class logical statements, which is crucial to reason abstractly about invariants and formulate atomic specifications.
The technical differences are discussed in <Ref>.
Thus we really make use of the fact that Iris is a higher-order logic—CaReSL is only a second-order logic and it would not be possible to make refinement judgments first-class in CaReSL (indeed Iris is not only based on CaReSL, but just as much on the higher-order iCAP logic of Svendsen and Birkedal [88]).
We also provide a mechanization in Coq with tactical support that supports the same backwards reasoning style that is employed for proving weakest preconditions in Iris [68].

Apart from the directions that we explored in this paper, there has been an abundance of work on logical relations models in Iris.
Binary logical relations models in Iris have been used for proving contextual equivalence in the context of Haskell's  monad [101], first-class per-thread continuations [96], and types-and-effect systems [66].
Unary logical relations models in Iris have been used for proving type safety and data-race freedom of the Rust type system [55, 32, 56], type safety of session types [49], type safety of Scala's core calculus DOT [45], and robust safety [90, 91].
Logical relations in Iris have also been used for showing other relational properties such as termination-preserving refinement [99], non-interference of concurrent programs [42], and recovery refinements (refinements in the presence of potential crashes) [27].
Nearly all of the aforementioned developments have accompanying mechanizations in Coq, and in some of those mechanizations the authors define their own tactics.
They define tactics for either their version of weakest preconditions or for derived operations, but, to the best of our knowledge, they do not define tactics for reasoning about the logical relation directly.

Relational logics.
Logics for proving relational properties of programs have a long history, going back to the earlier work of Plotkin and Abadi [80].
Since then many relational logics have been developed addressing various applications,
probabilistic properties in security [16, 17, 13] and cost analysis [24, 85].
Here we discuss some more recent work on relational logics that are capable of proving program refinements, with a focus on logics with support for higher-order languages, languages with mutable state, and languages with concurrency.

Earlier work on relational logics targeted programming languages with mutable state, but no concurrency.
Relational Hoare logic [15] and Relational Separation logic [107] can be used for reasoning about relational properties for first-order imperative programs, and they have inspired several extensions, for example to probabilistic languages [16].

Relational Higher Order Logic (RHOL) [3] is a recent relational higher-order logic for reasoning about relational properties of programs using relational refinement types.
The main judgment of RHOL allows one to prove that a relational formula $\varphi$ holds for two expressions, which do not necessarily have the same type.
While it is not directly possible to reason about expressions with different types in ,
we can relate them by using a type variable $\tvar$ and a suitable interpretation of $\tvar$ in the environment $\Delta$.
The authors prove soundness of RHOL and show how to embed a number of type systems into it.
They provide proofs of various relational properties such as non-interference and relative cost, as provided by the systems they embed into RHOL.
In our work we consider only one (family of) relation(s), namely the logical relation for contextual refinement.
The programming language considered in RHOL is a pure terminating variant of simply-typed PCF, while we consider a much richer programming language with general references and concurrency.

Liang and Feng developed a relational rely-guarantee style logic [71],
which can be used to prove refinement for fine-grained concurrent algorithms (including those with helping) but, in contrast
to , it can only be used to reason about first-order programs.

A relational logic for a sequential class-based language with dynamically allocated objects has been introduced by Banerjee  [19].
Their relational logic is based on region logic [20], a first-order logic, which is amenable to SMT-based automation.
Their relational logic is aimed at proving refinement and non-interference.
The approach was further extended in [76] to cover representation independence proofs using per-modules invariants and coupling relations.
In contrast, we focus on reasoning about refinements, but also treat concurrent programs and higher-order store, and we provide tool support for tactic-based interactive verification in Coq.

While not a logic in the strict sense, Relational Hoare Type Theory (RHTT) [75] is a dependent type theory for specification and verification of relational properties of higher-order programs with mutable first-order state, capable of expressing information flow and access control properties.
The object programming language of RHTT and the type system itself are shallowly embedded in Coq.

Atomic specifications.
To our knowledge, we are the first to study logically atomic specifications in the relational setting.
Logically atomic specifications originate in Hoare-style program logics.
Jacobs and Piessens [60] have originally developed a methodology for specifying logically atomic operations.
In their approach, specifications are parameterized by auxiliary code that is performed at the linearization point.
This approach was refined to what we refer to as HOCAP-style specifications, originally introduced in the context of the eponymous logic [89], where the role of auxiliary code is filled by view shifts [29], which in this paper are given by Iris's update modality $\vsW$ (<Ref>).
Compared to the original Jacobs-Piessens approach, in HOCAP-style specifications, the physical state that a logically atomic function operates on is hidden behind an abstract predicate.
Furthermore, HOCAP-style specifications can also be formulated for non-logically atomic operations, as we have seen in <Ref>.
The HOCAP-style specifications were later adopted in the iCAP logic [88] and Iris logic <cit.>.

Because Jacobs-Piessens and HOCAP-style specifications require parameterizing the (ghost) functions that are executed at the linearization points, such specifications are often referred to as higher-order.
As an alternative to this higher-order approach, da Rocha Pinto have introduced the notion of logically atomic triples in their program logic TaDA [36, 35].
Logically atomic triples are a first-order construct, built in as a primitive construct into the logic, which can be used to specify the atomic updates that a program performs.
The atomic triples can be systematically composed in the style of Hoare logic.
A more detailed comparison between the first-order and higher-order approach is given in [38].
TaDA-style logically atomic triples were adapted for Iris by Jung  [61, 59].
Specifically, they are encoded as derived constructs, using the Jacobs-Piessens approach, that satisfy the TaDA-style rules.

Speculative reasoning.
To facilitate speculative reasoning, we employ the mechanism for prophecy variables recently introduced in Iris [59].
Prophecy variables were first introduced by Abadi and Lamport [7] for the purpose of proving refinements of state machines.
The idea to use prophecy variables in program logic originates in the rely-guarantee style logic of Vafeiadis [103], although his treatment of prophecy variables is informal, and he appeals to Abadi and Lamport [7] for soundness.

Prophecy variables are not the only tool for carrying out speculative reasoning.
Both CaReSL [97] and extended LRG [71] are program logics capable of proving refinements of programs with future-dependent linearization points.
Both employ, albeit in different forms, a mechanism for recording multiple potential logical states of the program.
These multiple states can then be coalesced into a single one, once the linearization point is determined, and that resulting state is used for establishing the refinement.

Other approaches [63, 37] for proving linearizability of algorithms with future-dependent linearization points use Hoare logics with auxiliary state to track the abstract history of a program as a partial order.
The crucial property is that all total extensions of the partial order result in valid linear histories of the program.

Other work on linearizability.
One of the main application of is to prove linearizability of concurrent algorithms, by reducing it to contextual refinements.
Proving linearizability has a long history, and the program logic based approach is not the only one.
Other methods include automated model checking based solutions [70, 106, 26, 14]
and static analysis, in particular shape analysis, [10, 18, 104].
The model checking approaches in question do not prove linearizability, but automatically check execution traces for linearizability, bounding the heap or the number of threads.
Indeed, model checking approaches are designed to find bugs in a “push-button” fashion and can generate counterexample traces.
Approaches based on static analysis are usually sound even for unbounded heaps and threads, but limited to first-order programs.

§ DISCUSSION AND CONCLUSION

In this paper we have presented —the first mechanized relational logic for proving refinements of fine-grained concurrent higher-order programs.
We have demonstrated that is expressive enough to formally prove contextual refinements of concurrent programs in a modular way, by employing relational specifications of programs.
Moreover, the mechanization of in Coq allows us to carry out tactic-based interactive proofs in an intuitive way, by using 's type-directed structural rules and symbolic execution rules, coupled with the powerful mechanisms from Iris, such as invariants, ghost state, and prophecy variables.

In the remainder of this paper we discuss other case studies that we have mechanized in (<Ref>), discuss the “escape hatch” of (<Ref>) for verifying programs that cannot be handled by , and outline some directions for future work (<Ref>).

§.§ Other examples and case studies

In addition to the examples that we have presented in the paper, we have mechanized a number of examples from the literature on logical relations in in Coq.
Below we give a short summary of those examples.

* Linearizability of the Treiber stack [100];

* Refinement of higher-order cell objects from [69, 4];

* Refinement of a symbol lookup table and a name generation module from [4];

* Many equivalences from [33], adapted for the concurrent setting, including variations of the “awkward example” from [84], and the “higher-order profiling” example modified to use the atomic increment function $\FGincrement$;

* Equivalence between different ways of defining the fixed point combinators;

* Equivalence between late-choice and early-choice examples from [102];

* Algebraic laws for the parallel composition operation and its interaction with non-deterministic choice and sequential composition, inspired by the work on Concurrent Kleene Algebra [50];

* Linearizability of the Michael-Scott queue [74], mechanized by Friis Vindum and Birkedal [105].

§.§ The “escape hatch”

The rules of are sound, but not complete.
In particular, there are some examples that cannot be verified in completely.
One class of such examples that we know of, are refinements of fine-grained concurrent data structures with external linearization points (as opposed to fixed linearization points or future-dependent linearization points; see [30] for a survey outlining the differences).
Such external linearization points are present, for example, in algorithms that use helping or work-stealing.
Fortunately, 's model on top of Iris provides an “escape hatch” that still allows us to verify some data structures with helping.

In the appendix [41] we consider an example of such a data-structure: a fine-grained concurrent stack with helping, a simplified version of the elimination-backoff stack from [51].
We prove that this stack with helping refines a coarse-grained stack (thus showing that the stack with helping is linearizable).
The stack with helping is interesting because two threads that perform a push and pop operation concurrently can eliminate each other, by exchanging data through a side channel, thus reducing the contention for the top node of the stack.
To verify this example we make use of 's “escape hatch”—we unfold the definition of 's refinement judgment, and perform an explicit proof in terms of 's model in Iris so we can explicitly manipulate the ghost thread pool.
As we demonstrate, the “escape hatch” does not render useless for this example: we still use 's proof rules to carry out the majority of the proof.
Only for a small part of the proof we need to work in the model.
This is achieved by encapsulating the elimination mechanism of the stack, for which we can provide a logically atomic relational specification that is proved in the model of .
This specification can then be used through 's high-level rules to verify the complete data structure without further breaking the abstraction.

§.§ Future work

In future work we would like to examine the possibility of a more principled approach to specifying and verifying algorithms with helping, without having to reason in the model of .
In addition, it would be interesting to explore alternative approaches to speculative reasoning that do not involve prophecy variables.
Furthermore, we would like to study applications of to type-directed program transformations (for example typed closure conversion [2]) and message-passing programs (for example, by integration with the Iris-based Actris logic [47, 49]).

It would also be interesting to see how the ReLoC approach can be used for verifying other kinds of refinements, for example termination-sensitive refinements [99] or refinements in the presence of crashes [27].

§ ACKNOWLEDGMENTS

We thank the anonymous reviewers of this paper and the conference version at LICS'18 for their comments and suggestions.
We thank Herman Geuvers and Simon Friis Vindum for discussions,
and Amin Timany for his contributions to the linearizability proof of the stack with helping.

Dan Frumin was supported by the Dutch Research Council (NWO)
STW project 14319 (Sovereign) and VIDI Project No. 016.Vidi.189.046
(Unifying Correctness for Communicating Software).
Robbert Krebbers was supported by the Dutch Research Council (NWO), project 016.Veni.192.259.
Lars Birkedal was supported by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation and by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU).

[1]
Amal Ahmed, Andrew W. Appel, and Roberto Virga.
A stratified semantics of general references embeddable in
higher-order logic.
In LICS, pages 75–86, 2002.

[2]
Amal Ahmed and Matthias Blume.
Typed closure conversion preserves observational equivalence.
In ICFP, pages 157–168, 2008.

[3]
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and
Pierre-Yves Strub.
A relational logic for higher-order programs.
Journal of Functional Programming, 29:e16, 2019.

[4]
Amal Ahmed, Derek Dreyer, and Andreas Rossberg.
State-dependent representation independence.
In POPL, pages 340–353, 2009.

[5]
Amal Ahmed.
Semantics of types for mutable state.
PhD thesis, Princeton University, 2004.

[6]
Amal Ahmed.
Step-indexed syntactic logical relations for recursive and quantified
In ESOP, volume 3924 of LNCS, pages 69–83, 2006.

[7]
Martín Abadi and Leslie Lamport.
The existence of refinement mappings.
Theoretical Computer Science, 82(2):253–284, 1991.

[8]
Andrew W. Appel and David McAllester.
An indexed model of recursive types for foundational proof-carrying
TOPLAS, 23(5):657–683, 2001.

[9]
Andrew W. Appel, Paul-André Melliès, Christopher Richards, and
Jérôme Vouillon.
A very modal model of a modern, major, general type system.
In POPL, pages 109–122, 2007.

[10]
Daphna Amit, Noam Rinetzky, Thomas Reps, Mooly Sagiv, and Eran Yahav.
Comparison under abstraction for verifying linearizability.
In CAV, volume 4590 of LNCS, pages 477–490, 2007.

[11]
Lars Birkedal and Aleš Bizjak.
Lecture notes on iris: Higher-order concurrent separation logic.
<https://iris-project.org/tutorial-material.html>, 2020.

[12]
Lars Birkedal, Aleš Bizjak, and Jan Schwinghammer.
Step-indexed relational reasoning for countable nondeterminism.
Logical Methods in Computer Science, 9(4), 2013.

[13]
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César
Kunz, Benedikt Schmidt, and Pierre-Yves Strub.
Easycrypt: A tutorial.
In FOSAD, volume 8604 of LNCS, pages 146–166, 2013.

[14]
Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan.
Line-up: A complete and automatic linearizability checker.
In PLDI, pages 330–340, 2010.

[15]
Nick Benton.
Simple relational correctness proofs for static analyses and program
In POPL, pages 14–25, 2004.

[16]
Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin.
Formal certification of code-based cryptographic proofs.
In POPL, pages 90–101, 2009.

[17]
Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago
Zanella Béguelin.
Probabilistic relational reasoning for differential privacy.
In POPL, pages 97–110, 2012.

[18]
Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, and Mooly Sagiv.
Thread quantification for concurrent shape analysis.
In CAV, volume 5123 of LNCS, pages 399–413, 2008.

[19]
Anindya Banerjee, David A. Naumann, and Mohammad Nikouei.
Relational logic with framing and hypotheses.
In FSTTCS, volume 65 of LIPIcs, pages 11:1–11:16, 2016.

[20]
Anindya Banerjee, David A. Naumann, and Stan Rosenberg.
Local reasoning for global invariants, part I: Region logic.
JACM, 60(3):18:1–18:56, 2013.

[21]
Stephen Brookes.
A semantics for concurrent separation logic.
TCS, 375(1-3):227–270, 2007.

[22]
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob
Thamsborg, and Hongseok Yang.
Step-indexed Kripke models over recursive worlds.
In POPL, pages 119–132, 2011.

[23]
Lars Birkedal, Filip Sieczkowski, and Jacob Thamsborg.
A concurrent logical relation.
In CSL, volume 16 of LIPIcs, pages 107–121, 2012.

[24]
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan
Relational cost analysis.
In POPL, pages 316–329, 2017.

[25]
Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak Garg.
A type theory for incremental computational complexity with control
flow changes.
In ICFP, pages 132–145, 2016.

[26]
Pavol Černý, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri,
and Rajeev Alur.
Model checking of linearizability of concurrent list implementations.
In CAV, volume 6174 of LNCS, pages 465–479, 2010.

[27]
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich.
Verifying concurrent, crash-safe systems with perennial.
In SOSP, pages 243–258, 2019.

[28]
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
Logical step-indexed logical relations.
In LICS, pages 71–80, 2009.

[29]
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson,
and Hongseok Yang.
Views: Compositional reasoning for concurrent programs.
In POPL, pages 287–300, 2013.

[30]
Brijesh Dongol and John Derrick.
Verifying linearizability: A comparative survey.
ACM Computing Surveys, 48(2):19:1–19:43, 2015.

[31]
Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, and
Viktor Vafeiadis.
Concurrent abstract predicates.
In ECOOP, volume 6183 of LNCS, pages 504–528, 2010.

[32]
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek
RustBelt meets relaxed memory.
PACMPL, 4(POPL):34:1–34:29, 2020.

[33]
Derek Dreyer, Georg Neis, and Lars Birkedal.
The impact of higher-order state and control effects on local
relational reasoning.
Journal of Functional Programming, 22(4-5):477–528, 2012.

[34]
Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal.
A relational modal logic for higher-order stateful ADTs.
In POPL, pages 185–198, 2010.

[35]
Pedro da Rocha Pinto.
Reasoning with time and data abstractions.
PhD thesis, Imperial College London, 2017.

[36]
Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner.
TaDA: A logic for time and data abstraction.
In ECOOP, volume 8586 of LNCS, pages 207–231, 2014.

[37]
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya
Concurrent data structures linked in time.
In ECOOP, volume 74 of LIPIcs, pages 8:1–8:30, 2017.

[38]
Thomas Dinsdale-Young, Pedro da Rocha Pinto, and Philippa Gardner.
A perspective on specifying and verifying concurrent modules.
Journal of Logical and Algebraic Methods in Programming,
98:1–25, August 2018.

[39]
Matthias Felleisen and Robert Hieb.
The revised report on the syntactic theories of sequential control
and state.
Theoretical Computer Science, 103(2):235–271, 1992.

[40]
Dan Frumin, Robbert Krebbers, and Lars Birkedal.
ReLoC: A mechanised relational logic for fine-grained concurrency.
In LICS, pages 442–451, 2018.

[41]
Dan Frumin, Robbert Krebbers, and Lars Birkedal.
Appendix and Coq development of ReLoC, 2021.
Available at <https://iris-project.org/reloc/>.

[42]
Dan Frumin, Robbert Krebbers, and Lars Birkedal.
Compositional non-interference for fine-grained concurrent programs,
To appear in Security & Privacy 2021.

[43]
Ivana Filipović, Peter O'Hearn, Noam Rinetzky, and Hongseok Yang.
Abstraction for concurrent objects.
Theoretical Computer Science, 411(51-52):4379–4398, 2010.

[44]
Andrew D. Gordon.
Bisimilarity as a theory of functional programming.
Theoretical Computer Science, 228(1-2):5–47, 1999.

[45]
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert
Scala step-by-step: Soundness for DOT with step-indexed logical
relations in Iris, 2020.

[46]
Robert Harper.
Practical Foundations for Programming Languages (2nd. Ed.).
Cambridge University Press, 2016.

[47]
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers.
Actris: Session-type based reasoning in separation logic.
PACMPL, 4(POPL):6:1–6:30, 2020.

[48]
Chung-Kil Hur and Derek Dreyer.
A Kripke logical relation between ML and assembly.
In POPL, pages 133–146, 2011.

[49]
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper
Machine-checked semantic session typing, 2021.
To appear at CPP'21.

[50]
Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman.
Concurrent Kleene algebra and its foundations.
The Journal of Logic and Algebraic Programming, 80(6):266–296,

[51]
Danny Hendler, Nir Shavit, and Lena Yerushalmi.
A scalable lock-free stack algorithm.
In SPAA, pages 206–215, 2004.

[52]
Maurice Herlihy and Jeannette Wing.
Linearizability: A correctness condition for concurrent objects.
TOPLAS, 12(3):463–492, 1990.

[53]
Samin Ishtiaq and Peter O'Hearn.
BI as an assertion language for mutable data structures.
In POPL, pages 14–26, 2001.

[54]
Iris team.
The Iris Project website and Coq development, 2020.

[55]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer.
RustBelt: Securing the foundations of the Rust programming
PACMPL, 2(POPL):66:1–66:34, 2018.

[56]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer.
Safe systems programming in Rust: The promise and the challenge,
To appear in CACM.

[57]
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer.
Higher-order ghost state.
In ICFP, pages 256–269, 2016.

[58]
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars
Birkedal, and Derek Dreyer.
Iris from the ground up: A modular foundation for higher-order
concurrent separation logic.
Journal of Functional Programming, 28:e20, 2018.

[59]
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin
Timany, Derek Dreyer, and Bart Jacobs.
The future is ours: prophecy variables in separation logic.
PACMPL, 4(POPL):45:1–45:32, 2020.

[60]
Bart Jacobs and Frank Piessens.
Expressive modular fine-grained concurrency specification.
In POPL, pages 271–282, 2011.

[61]
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars
Birkedal, and Derek Dreyer.
Iris: Monoids and invariants as an orthogonal basis for concurrent
In POPL, pages 637–650, 2015.

[62]
Patricia Johann, Alex Simpson, and Janis Voigtländer.
A generic operational metatheory for algebraic effects.
In LICS, pages 209–218, 2010.

[63]
Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson.
Proving linearizability using partial orders.
In ESOP, volume 10201 of LNCS, pages 639–667, 2017.

[64]
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek
Dreyer, and Lars Birkedal.
The essence of higher-order concurrent separation logic.
In ESOP, volume 10201 of LNCS, pages 696–723, 2017.

[65]
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer.
MoSeL: A general, extensible modal framework for interactive proofs
in separation logic.
PACMPL, 2(ICFP):77:1–77:30, 2018.

[66]
Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal.
A relational model of types-and-effects in higher-order concurrent
separation logic.
In POPL, pages 218–231, 2017.

[67]
Dexter Kozen.
A completeness theorem for kleene algebras and the algebra of regular
Information and Computation, 110(2):366–390, 1994.

[68]
Robbert Krebbers, Amin Timany, and Lars Birkedal.
Interactive proofs in higher-order concurrent separation logic.
In POPL, pages 205–217, 2017.

[69]
Vasileios Koutavas and Mitchell Wand.
Small bisimulations for reasoning about higher-order imperative
In POPL, pages 141–152, 2006.

[70]
Yang Liu, Wei Chen, Yanhong A. Liu, and Jun Sun.
Model checking linearizability via refinement.
In FM, volume 5850 of LNCS, pages 321–337, 2009.

[71]
Hongjin Liang and Xinyu Feng.
Modular verification of linearizability with non-fixed linearization
In PLDI, pages 459–470, 2013.

[72]
John Mitchell.
Representation independence and data abstraction.
In POPL, pages 263–276, 1986.

[73]
John M. Mellor-Crummey and Michael L. Scott.
Algorithms for scalable synchronization on shared-memory
TOCS, 9(1):21–65, 1991.

[74]
Maged Michael and Michael Scott.
Simple, fast, and practical non-blocking and blocking concurrent
queue algorithms.
In PODC, pages 267–275, 1996.

[75]
Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg.
Dependent type theory for verification of information flow and access
control policies.
TOPLAS, 35(2):6:1–6:41, 2013.

[76]
Mohammad Nikouei, Anindya Banerjee, and David A. Naumann.
Data Abstraction and Relational Program Logic.
arXiv e-prints, page arXiv:1910.14560, October 2019.

[77]
Georg Neis, Derek Dreyer, and Andreas Rossberg.
Non-parametric parametricity.
Journal of Functional Programming, 21(4-5):497–562, 2011.

[78]
Peter W. O'Hearn.
Resources, concurrency, and local reasoning.
TCS, 375(1-3):271–307, 2007.

[79]
Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang.
Local reasoning about programs that alter data structures.
In CSL, volume 2142 of LNCS, pages 1–19, 2001.

[80]
Gordon Plotkin and Martín Abadi.
A logic for parametric polymorphism.
In TLCA, volume 664 of LNCS, pages 361–375, 1993.

[81]
Andrew M. Pitts.
Operational semantics and program equivalence.
In APPSEM, volume 2395 of LNCS, pages 378–412, 2000.

[82]
Andrew M. Pitts.
Typed operational reasoning.
In Benjamin C. Pierce, editor, Advanced Topics in Types and
Programming Languages, chapter 7, pages 245–289. MIT Press, 2005.

[83]
Gordon Plotkin.
A powerdomain construction.
SIAM Journal on Computing, 5(3):452–487, 1976.

[84]
Andrew M. Pitts and Ian Stark.
Operational reasoning for functions with local state.
In Higher Order Operational Techniques in Semantics, pages
227–274. Cambridge University Press, 1998.

[85]
Ivan Radiček, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian
Monadic refinements for relational cost analysis.
PACMPL, 2(POPL):36:1–36:32, 2018.

[86]
John C. Reynolds.
Towards a theory of type structure.
In Programming Symposium, Proceedings Colloque sur la
Programmation, Paris, volume 19 of LNCS, pages 408–423, 1974.

[87]
Vineet Rajani and Deepak Garg.
Types for information flow control: Labeling granularity and semantic
In CSF, pages 233–246. IEEE, 2018.

[88]
Kasper Svendsen and Lars Birkedal.
Impredicative concurrent abstract predicates.
In ESOP, volume 8410 of LNCS, pages 149–168, 2014.

[89]
Kasper Svendsen, Lars Birkedal, and Matthew Parkinson.
Modular reasoning about separation of concurrent data structures.
In ESOP, volume 7792 of LNCS, pages 169–188, 2013.

[90]
David Swasey, Deepak Garg, and Derek Dreyer.
Robust and compositional verification of object capability patterns.
PACMPL, 1(OOPSLA):89:1–89:26, 2017.

[91]
Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak.
The high-level benefits of low-level sandboxing.
PACMPL, 4(POPL):32:1–32:32, 2020.

[92]
Michael Smyth.
In International Symposium on Mathematical Foundations of
Computer Science, pages 537–543. Springer, 1976.

[93]
Eijiro Sumii and Benjamin C. Pierce.
A bisimulation for type abstraction and recursion.
JACM, 54(5):26, 2007.

[94]
Steven Schäfer, Tobias Tebbi, and Gert Smolka.
Autosubst: Reasoning with de Bruijn terms and parallel
In ITP, volume 9236 of LNCS, pages 359–374, 2015.

[95]
Alex Simpson and Niels Voorneveld.
Behavioural equivalence via modalities for algebraic effects.
TOPLAS, 42(1):4:1–4:45, 2020.

[96]
Amin Timany and Lars Birkedal.
Mechanized relational verification of concurrent programs with
PACMPL, 3(ICFP):105:1–105:28, 2019.

[97]
Aaron Turon, Derek Dreyer, and Lars Birkedal.
Unifying refinement and Hoare-style reasoning in a logic for
higher-order concurrency.
In ICFP, pages 377–390, 2013.

[98]
Amin Timany.
Contributions in programming languages theory: Logical relations
and type theory.
PhD thesis, KU Leuven, 2018.

[99]
Joseph Tassarotti, Ralf Jung, and Robert Harper.
A higher-order logic for concurrent termination-preserving
In ESOP, volume 10201 of LNCS, pages 909–936, 2017.

[100]
R. Kent Treiber.
Systems programming: Coping with parallelism.
Technical report, Thomas J. Watson Research Center, 1986.

[101]
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal.
A logical relation for monadic encapsulation of state: proving
contextual equivalences in the presence of runST.
PACMPL, 2(POPL):64:1–64:28, 2018.

[102]
Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer.
Logical relations for fine-grained concurrency.
In POPL, pages 343–356, 2013.

[103]
Viktor Vafeiadis.
Modular fine-grained concurrency verification.
PhD thesis, University of Cambridge, 2008.

[104]
Viktor Vafeiadis.
Shape-value abstraction for verifying linearizability.
In VMCI, volume 5403 of LNCS, pages 335–348, 2009.

[105]
Simon Friis Vindum and Lars Birkedal.
Contextual refinement of the michael-scott queue (proof pearl), 2021.
To appear at CPP'21.

[106]
Martin Vechev, Eran Yahav, and Greta Yorsh.
Experience with model checking linearizability.
In SPIN, volume 5578 of LNCS, pages 261–278, 2009.

[107]
Hongseok Yang.
Relational separation logic.
Theoretical Computer Science, 375(1-3):308–334, 2007.


# Feedback Pulses

Vishesh Kaushik†, Navin Khaneja To whom correspondence may be addressed.
<EMAIL_ADDRESS>and Control Engineering, IIT Bombay, Powai
- 400076, India.

Abstract

We have a new paradigm to design NMR pulses. Pulses, we call feedback pulses.
We want broadband inversion and excitation. We have many offsets, start
evolving them all starting from the north pole. Monitor them on the Bloch
sphere, see which offset is worst (most away from south pole). Change the rf-
phase to the offset ($\pi/2$ ahead of offset transverse magnetization phase)
and irradiate at that offset frequency and evolve for some time and monitor
and repeat, looking for worst offset. When we are on resonance to a offset, we
are doing well, inverting it and when we are off resonant, we don’t hurt much
(even if hurt little, we will come back to the offset in good time). By the
process of monitoring, and setting phase we eventually push everything to the
south pole and bingo, we have an inversion pulse. Feedback is done in
simulation, but what results in end is a broadband inversion pulse. For
broadband excitation, start with all offsets (symmetric around origin) on y
axis. By feedback push them to the south pole. When we run the resulting
sequence backward with phases, $\pi$ incremented, we will get an excitation
pulse. For band-selective excitation pulse put offsets in pass band on the $y$
axis and in the stop band on the south pole. Use feedback to push everything
to the south pole. Again, run backwards with $\pi$ incremented phases, to get
band selective excitation. Suddenly, we have it all, simple and easy. The
paper, introduces the feedback pulse algorithm, simulations and experiments.

##  1 Introduction

The excitation and inversion pulse is ubiquitous in Fourier Transform-NMR,
being the starting point of all experiments. With increasing field strengths,
in high resolution NMR, sensitivity and resolution comes with the challenge of
uniformly exciting or inverting larger bandwidths. At a field of 1 GHz, the
target bandwidth is $50$ kHz for excitation of entire 200 ppm 13C chemical
shifts. The required $25$ kHz hard pulse exceeds the capabilities of most 13C
probes and poses additional problems in phasing the spectra. In 19F NMR,
chemical shifts can range over 600 ppm, which requires excitation of different
regions of the spectra. Methods that can achieve uniform excitation over the
entire bandwidth in 19F NMR, are therefore most desirable. Towards this end,
several methods have been developed for broadband excitation/inversion, which
have reduced the phase variation of the excited magnetization as a function of
the resonance offset. These include composite pulses, adiabatic sequences,
polycromatic sequences, phase alternating pulse sequences, optimal control
pulse design, and method of multiple frames, [1]-[20].

Another application is frequency (band) selective excitation. Frequency-
selective pulses have widespread use in magnetic resonance and significant
effort has been devoted towards their design [21]-[67]. Several experiments in
high-resolution NMR and magnetic resonance imaging require radio-frequency
pulses which excite NMR response over a prescribed frequency range with
negligible effects elsewhere. Such band-selective pulses are particularly
valuable when the excitation is uniform over desired bandwidth and of constant
phase.

In this paper, we introduce a new paradigm for NMR pulse design, the concept
of feedback pulses. In classical control, feedback is the way to go. Whether
it is regulating speed of a car, or opening a control valve by certain amount,
or setting temperature in a room or changing missile course by $5^{\circ}$ or
steering a rocket to moon, feedback is the default design method. The
parameters of a system dynamics are not always exactly known and in order to
steer the system to a target state, we don’t apply a known control pulse from
a library, instead we monitor the system and measure its current value and
nudge it in direction of target and keep doing it till it is at target. We use
the same idea to design broadband excitation and inversion pulses. We want
broadband inversion and excitation. We have many offsets, start evolving them
all starting from north pole. Monitor them on Bloch sphere, see which offset
is worst (most away from south pole). Change the rf-phase to the offset and
irradiate at that offset frequency and evolve for some time and monitor and
repeat, looking for worst offset. When we are on resonance to a offset, we are
doing well, inverting it and when we are off resonant, we don’t hurt much. By
process of monitoring, setting phase we eventually push everything to south
pole and we have a inversion pulse. For broadband excitation, start with all
offsets (symmetric around origin) on y axis. By feedback push them to the
south pole. When we run the resulting sequence backward with phases, $\pi$
incremented, we will get an excitation pulse. For band-selective pulse put
offsets in pass band on the $y$ axis and in the stop band on the south pole.
Use feedback to push everything to the south pole. Again run backwards, with
$\pi$ incremented phases, to get selective excitation. The paper introduces
this feedback pulse algorithm, simulation and experiments.

##  2 Theory and Experiments

###  2.1 Algorithm

Let $A$ be amplitude of rf pulse. Let $(z_{j},\phi_{j})$ be the $z$ coordinate
and phase of transverse magnetization for the $j^{th}$ offset (where offsets
lie in range $[-B,B]$). Start with all $z_{j}=1$ (north pole). Find $j$ with
target $z_{j}$ (most away from south pole), change rf pulse phase to
$\theta_{i}=\phi_{j}+\frac{\pi}{2}$ and give a pulse of small flip angle
$\alpha=\frac{1}{2}$ degree and repeat and continue till all $z_{j}$ are near
south pole then stop. Then $\theta_{i}$ is the broadband inversion pulse.

Let $(z_{j},\phi_{j})$ be the $z$ coordinate and phase of transverse
magnetization for the $j^{th}$ offset. Start with all
$z_{j}=0,\phi_{j}=90^{\circ}$ (y axis). Find $j$ with largest $z_{j}$ , change
rf pulse phase to $\theta_{i}=\phi_{j}+\frac{\pi}{2}$ and give a pulse of
small flip angle say $\alpha=\frac{1}{2}$ degree and repeat and continue till
all $z_{j}$ are near south pole then stop. Then
$\theta_{i}=\theta_{n-i}+180^{\circ}$ is the broadband x-excitation pulse, as
the offset $\omega$ will backtrack the trajectory of $-\omega$ and go back
from pole to equator.

Let $(z_{j},\phi_{j})$ be the $z$ coordinate and phase of transverse
magnetization for the $j^{th}$ offset (where offsets lie in range $[-B,B]$,
with $[-C,C]$ as pass band and outside stop band). Start with all
$z_{j}=0,\phi_{j}=90^{\circ}$ (y axis) for pass band and $z_{j}=-1$ (south
pole) for stop band. Find $j$ with largest $z_{j}$ , change rf pulse phase to
$\theta_{i}=\phi_{j}+\frac{\pi}{2}$ and give a pulse of small flip angle say
$\frac{1}{2}$ degree and repeat and continue till all $z_{j}$ are near south
pole then stop. Then $\theta_{i}=\theta_{n-i}+180^{\circ}$ is the band
selective x-pulse.

###  2.2 Simulations

In above, for broadband inversion and excitation, $A=10$ kHz, $B=20$ kHz,
$\alpha=.57^{\circ}$. Fig. 1 and 2 shows $x$, $y$, $z$ coordinates as function
of offset after application of broadband inversion and excitation. Also shown
are the rf-phases. The two sequences take 3 ms and 2 ms respectively and have
18907 and 12587 number of phases respectively. We used 40 offsets in the
range.

In above, for band selective excitation, $A=5$ kHz, $B=5$ kHz, $C=2$ kHz,
$\alpha=.29^{\circ}$. Fig. 3 shows $x$, $y$, $z$ coordinates as function of
offset after application of selective excitation. Also shown are the rf-
phases. The sequence takes 6.7 ms and have 41812 number of phases.

Figure 1: Fig. depicts inversion with feedback pulses over a bandwidth of $40$
kHz with rf amplitude $10$ kHz and time of pulse 3 ms. Figure 2: Fig. depicts
excitation with feedback pulses over a bandwidth of $40$ kHz with rf amplitude
$10$ kHz and time of pulse 2 ms. Figure 3: Fig. depicts selective excitation
with feedback pulses over a bandwidth of $4$ kHz with rf amplitude $5$ kHz and
time of pulse 6.7ms .

Based on simulations, experiments for broadband inversion, excitation and band
selective excitation were performed on a $99.5\%$ D20 and$.5\%$ H20 solution.
Water resonance at 4.7 ppm is excited as different offsets by varying
transmitter frequency. Fig. 4, 5 and 6, shows experimental inversion,
excitation and band selective profiles respectively.

Figure 4: Fig. depicts 40 kHz wide inversion profile (HDO signal) of feedback
inversion pulse on a sample of $99.5\%$ D20 and$.5\%$ H20\. Rf power is $10$
kHz and pulse is 3 ms long. Figure 5: Fig. depicts 40 kHz wide excitation
profile of feedback inversion pulse on a sample of $99.5\%$ D20 and$.5\%$
H20\. Rf power is $10$ kHz and pulse is 2 ms long. Figure 6: Fig. depicts 4
kHz wide selective excitation profile of selective pulse on a sample of
$99.5\%$ D20 and$.5\%$ H20\. Rf power is $5$ kHz and pulse is 6.7 ms long.

##  3 Conclusion

In this paper, we introduced a new paradigm for design of NMR pulses, the
pulses we call feedback pulses. By monitoring, the offsets and setting the
phase of the rf-pulse to an offset, we can talk to it and drive it south pole
and repeat the process to engineer broadband inversion, excitation and
selective excitation pulses. We provided algorithms, simulations and
experiments to validate this methodology.

In classical control feedback is a popular method. Whether it is regulating
speed of car, or opening a control valve, or setting temperature in a room or
guiding a missile or steering a rocket to moon, feedback is the default design
method. The parameters of a system dynamics are not always exactly known and
in order to steer the system to a target state we don’t apply a known control
pulse from a library, instead we monitor the system and measure its current
value and nudge it in direction of target and keep doing it till it is at
target.

It is expected the feedback method proposed in this paper will find widespread
use in other applications in NMR like frequency selective excitation with
arbitrary profile with multiple bands, design of broadband propagators (like
refocusing pulses) and rf-inhomogeneity compensation. In our implementation,
we monitor the worst offset, in other and future implementations we may choose
different polling strategy, by going through the offsets in a linear order (as
in a chirp) and setting the phase to a offset as we go and poll it and
repeating the process, till all offsets are on south pole.

##  4 Acknowledgement

We thank Prof. Ashutosh Kumar and Pramod Mali in HFNMR lab at IIT Bombay for
their help with NMR data collection.

## References

  * [1] R. Freeman, S. P. Kempsell, M.H. Levitt, Radio frequency pulse sequence which compensate their own imperfections, J. Magn. reson. 38 (1980) 453-479.
  * [2] M.H. Levitt, Symmetrical composite pulse sequences for NMR population inversion. I. Compensation of radiofrequency field inhomogeneity, J. Magn. Reson. 48 (1982) 234-264.
  * [3] M.H. Levitt, R. R. Ernst, Composite pulses constructed by a recursive expansion procedure, J. Magn. Reson. 55(1983) 247-254
  * [4] R. Tycho, H.M. Cho, E. Schneider, A. Pines, Composite Pulses without phase distortion, J. Magn. Reson. 61(1985)90-101.
  * [5] M.H. Levitt, Composite Pulses, Prog. Nucl. Magn. Reson. Spectrosc. 18(1986) 61-122.
  * [6] A.J. Shaka, A. PinesSymmetric phase-alternating composite pulses, J. Magn. Reson. 71(1987) 495-503.
  * [7] J.-M. Böhlen, M. Rey, G. Bodenhausen, Refocusing with chirped pulses for broadband excitation without phase dispersion, J. Magn. Reson. 84 (1989) 191-197.
  * [8] J.-M. Böhlen, G. Bodenhausen, Experimental aspects of chirp NMR spectroscopy, J. Magn. Reson. Ser. A. 102(1993)293-301.
  * [9] D. Abramovich, S. Vega, Derivation of broadband and narrowband excitation pulses using the Floquet formalism, J. Magn. Reson. Ser. A. 105(1993)30-48.
  * [10] E. Kupce, R. Freeman, Wideband excitation with polychromatic pulses, J. Magn.Reson. Ser. A. 108(1994) 268-273.
  * [11] K. Hallenga, G. M. Lippens, A constant-time 13C-1H HSQC with uniform excitation over the complete 13C chemical shift range, J. Biomol. NMR 5(1995) 59-66.
  * [12] T. L. Hwang, P.C.M van Zijl, M. Garwood, Broadband adiabatic refocusing without phase distortion, J. Magn. Reson. 124 (1997)250-254.
  * [13] K.E. Cano, M.A. Smith, A.J. Shaka, adjustable, broadband, selective excitation with uniform phase, J. Magn. Reson. 155 (2002) 131-139.
  * [14] J. Baum, R. Tycko, A. Pines, Broadband and adiabatic inversion of a two level system by phase modulated pulses, Phys. rev. A. 32 (1985) 3435-3447.
  * [15] T.E. Skinner, T. O. Reiss, B. Luy, N. Khaneja, S. J. Glaser, Application of optimal control theory to the design of broadband excitation pulses for high-resolution NMR, J. Magn. Reson. 163 (2003) 8-15.
  * [16] T. E. Skinner, K. Kobzar, B. Luy, M. R. Bendall, W. Bermel, N. Khaneja, and S. J. Glaser, Optimal control design of constant amplitude phase-modulated pulses: application to calibration-free broadband excitation, Journal of Magnetic Resonance. 179 (2006) 241.
  * [17] K. Kobzar, T.E. Skinner, N. Khaneja, S. J. Glaser, B. Luy, Exploring the limits of broadbad excitation and inversion:II. Rf-power optimized pulses, J. Magn. Reson., 194(1), 58-66, (2008).
  * [18] J. E. Power, M. Foroozandeh, R.W. Adams, M. Nilsson, S.R. Coombes, A.R. Phillips, G. A. Morris, Increasing the quantitative bandwidth of NMR measurements, DOI: 10.1039/c5cc10206e, Chem. Commun. (2016).
  * [19] M.R.M. Koos, H. Feyrer, B. Luy, Broadband excitation pulses with variable RF amplitude-dependent flip angle (RADFA), Magn. Reson. Chem., Vol. 53, Issue 11, pp 886-893, 2015.
  * [20] N. Khaneja, A. Dubey, H.S. Atreya, Ultra broadband NMR spectroscopy using multiple rotating frame technique, J. Magn. Reson. 265(2016) 117-128.
  * [21] B. L. Tomlinson and H. D. W. Hill, Fourier synthesized excitation of nuclear magnetic resonance with application to homonuclear decoupling and solvent line suppression, J. Chem. Phys. 59, (1973) 1775-1785.
  * [22] G. Bodenhausen, R. Freeman G. A. Morris, A simple pulse sequence for selective excitation in Fourier transform NMR, J. Magn. Reson. 23 (1976) 171-175.
  * [23] G. A. Morris and R. freeman, Selective excitation in Fourier transform nuclear magnetic resonance, J. Magn. Reson. 29 (1978) 433-462.
  * [24] D. I. Hoult, The solution of the Bloch equations in the presence of a varying B1 field: An approach to selective pulse analysis, J. Magn. Reson. 35 (1979) 68-86.
  * [25] L. Emsley, G. Bodenhausen, Self-refocussing effect of 270 Gaussian pulses. Applications to selective two-dimensional exchange spectroscopy, J. Magn. Resonance. 82 (1989) 211-221.
  * [26] P. Caravatti, G. Bodenhausen, R. R. Ernst, Selective pulse experiments in high resolution solid state NMR, J. Magn. Reson. 55 (1983) 88-103.
  * [27] C. Bauer, R. Freeman, T. Frenkiel, J. Keeler, A.J. Shaka, Gaussian pulses, J. Magn. Reson. 58 (1984) 442-457.
  * [28] M.S. Silver, R.I. Joseph, D.I. Hoult, Highly selective $\frac{\pi}{2}$ and $\pi$pulse generation. J. Magn. Reson. 59 (1984) 347-351.
  * [29] J. Friedrich, S. Davies, R. Freeman, Shaped selective pulses for coherence-transfer experiments, J. magn. Reson. 75 (1987) 390-395.
  * [30] C.J. Hardy, P.A. Bottomley, M. O Donnell, and P. Roemer, Optimization of two dimensional spatially selective NMR pulses by simulated annealing, J. Magn. Reson. 77 (1988) 223-250.
  * [31] F. Loaiza, M. A. McCoy, S. L. Hammes, W. S. Warren, Selective excitation without phase distortion using self-refocused amplitude- and amplitude/phase-modulated pulses, J. Magn. Reson. 77 (1988) 175-181.
  * [32] P. Tekely, J. Brondeau, K. Elbayed, A. Retournard and, D. Canet, A simple pulse train, using 90 hard pulses, for selective excitation in high-resolution solid-state NMR, J. Magn. Reson. 80 (1988) 509-516.
  * [33] X.-L. Wu, R. Freeman, Darwins ideas applied to mag- netic resonance. The marriage broker, J. Magn. Reson. 85 (1989) 414-420.
  * [34] H. Geen, S. Wimperis, R. Freeman, Band-selective pulses without phase distortion. A simulated annealing approach, J. Magn. Reson. 85 (1989) 620-627.
  * [35] L. Emsley and G. Bodenhausen, Self-refocusing 270 gaussian pulses for slice selection without gradient reversal in magnetic resonance imaging, Magn, Reson.Med. 10 (1989) 273-281.
  * [36] A.E. Yagle, Inversion of the Bloch transform in magnetic resonance imaging using asymmetric two- component inverse scattering, Inverse Problem 6 (1990) 133-151.
  * [37] M. Shinnar, L. Bolinger, J. S. Leigh, The synthesis of pulse sequences yielding arbitrary magnetization vectors, Mag. Reson. Med. 12 (1989) 74-80.
  * [38] M. Shinnar, L. Bolinger, J. S. Leigh, The use of finite impulse response filters in pulse design, Mag. Reson. Med. 12 (1989) 81-87.
  * [39] M. Shinnar, J. S. Leigh, The application of spinors to pulse synthesis and analysis, Mag. Reson. Med. 12 (1989) 93-98.
  * [40] J. Pauly, P. Le Roux, D. Nishimur, A. Macovski, Parameter relations for the Shinnar-Le Roux selective excitation pulse design algorithm, IEEE Trans. Med. Imag. 10 (1991) 53-65.
  * [41] J.W.Carlson, Exact solution for selective-excitation pulses. J. Magn. Reson. 94 (1991) 376-386.
  * [42] H. Geen and R. Freeman, Band-selective radiofrequency pulses. J. Magn. Reson. 93 (1991) 93-141.
  * [43] R. Freeman, Selective excitation in high-resolution NMR, Chem. Rev. 91-7 (1991) 1397-1412.
  * [44] R. Freeman, High resolution NMR using selective excitation, J. Mol. Struct, 266 (1992) 39-51.
  * [45] J.W.Carlson, Exact solution for selective-excitation pulses. II Excitation pulses with phase control. J. Magn. Reson.97 (1992) 65-78.
  * [46] D.E.Rourke and P.G.Morris, The inverse scattering and its use in the exact inversion of the Bloch equation for noninteracting spins. J. Magn. Reson. 99 (1992) 118-138.
  * [47] L. Emsley, G. Bodenhausen, Optimization of shaped selective pulses for NMR using a quaternion description of their overall propagators, J. Magn. Reson. 97 (1992) 135-148.
  * [48] E. Kupce, R.Freeman, Polychromatic selective pulses, J. Magn. Reson. Ser.A 102 (1993) 122-126.
  * [49] D.E. Rourke, M.J.W. Prior, P.G. Morris, J.A.B. Lohman, Stereographic projection method of exactly calculating selective pulses, J. Magn. Reson. A 107 (1994) 203-214.
  * [50] L. Emsley, Selective pulses and their applications to as- signment and structure determination in nuclear magnetic resonance, Methods Enzymol. 239 (1994) 207-246.
  * [51] E. Kupce, R. Freeman, Band-Selective Correlation Spectroscopy, J. Magn. Reson. A 112 (1995) 134-137.
  * [52] E. Kupce, J. Boyd, I.D. Campbell, Short selective pulses for biochemical applications, J. Magn. Reson. Series B 106 (1995) 300-303.
  * [53] S. Caldarelli, A. Lesage, L. Emsley, Pure-phase selective excitation in NMR by acquisition during the pulse, J.Magn. Reson. A 116 (1995) 129-132.
  * [54] C. Dalvit, S. Y. Ko, J.-M. Böhlen, Single and multiple- selective excitation combined with pulsed field gradients, J. Magn. Reson. B 10 (1996) 124-131.
  * [55] P. Borgnat, A. Lesage, S. Caldarelli, L. Emsley, Narrow- band linear selective pulses for NMR, J. Magn. Reson.A 119 (1996) 289-294.
  * [56] E. Lunati, P. Cofrancesco, M. Villa, P. Marzola, F. Osculati, Evolution Strategy Optimization for Selective Pulses in NMR, J. Magn. Reson. 134 (1998) 223-235.
  * [57] T. Parella, F. Snchez-Ferrando, A. Virgili, A simple ap- proach for ultraclean multisite selective excitation using excitation sculpting, J. Magn. Reson. 135 (1998) 50-53.
  * [58] Ray Freeman, Shaped radiofrequency pulses in high resolution NMR, Prog. Nucl. Magn. Reson. Spectrosc. 32, (1998) 59-106.
  * [59] P. Xu, X.-L. Wu, R. Freeman, User-friendly selective pulses, J. Magn. Reson. 99 (1992) 308-322.
  * [60] M. A. McCoy, L. Mueller, Nonresonant effects of frequency-selective pulses, J. Magn. Reson. 99 (1992) 18-36.
  * [61] C. Roumestand,C. Delay, J. A. Gavid, D. Canet, A practical approach to the implementation of selectivity in homonuclear multidimensional NMR with frequency selective-filtering techniques. Application to the chem- ical structure elucidation of complex oligosaccharides (pages 451478), Magn. Reson. Chem. 37 (1999) 451-478.
  * [62] C. Roumestand, D. Canet, Extending the excitation sculpting concept for selective excitation, J. Magn. Re- son. 147 (2000) 331-339.
  * [63] K. Zangger, M. Oberer, H. Sterk, Pure-phase selective excitation in fast-relaxing systems, J. Magn. Reson. 152 (2001) 48-56.
  * [64] P. Charmont, D. Sakellariou, L. Emsley, Sample restric- tion using radiofrequency field selective pulses in highresolution solid-state NMR, J. Magn. Reson. 154 (2002) 136-141.
  * [65] K. E. Cano, M. A. Smith, A. J. Shaka, Adjustable, broadband, selective excitation with uniform phase, J. Magn. Reson. 155 (2002) 131-139.
  * [66] M. Veshtort, R. Griffin, High-performance selective ex- citation pulses for solid-and liquid-state NMR spectroscopy, Chem. Phys. Chem. 5 (2004) 834-850.
  * [67] T. E. Skinner, N. I. Gershenzon, M. Nimbalkar, S. J. Glaser, Optimal control design of band selective excitation pulses that accommodate relaxation and RF inhomogeneity, J. Magn. reson. 217 (2012) 53-60.