# Random forest prediction of Alzheimer’s disease using
pairwise selection from time series data.

P.J. Moore111Postdoc, Mathematical Institute, University of Oxford.
<EMAIL_ADDRESS>J. Gallacher222Professor, Department of Psychiatry,
University of Oxford. T.J. Lyons 333Professor, Mathematical Institute,
University of Oxford.
for the Alzheimer’s Disease Neuroimaging Initiative 444Data used in
preparation of this article were obtained from the Alzheimer’s Disease
Neuroimaging Initiative (ADNI) database (adni.loni.usc.edu). As such, the
investigators within the ADNI contributed to the design and implementation of
ADNI and/or provided data but did not participate in analysis or writing of
this report. A complete listing of ADNI investigators can be found
at:http://adni.loni.usc.edu/. University of Oxford

###### Abstract

Time-dependent data collected in studies of Alzheimer’s disease usually has
missing and irregularly sampled data points. For this reason time series
methods which assume regular sampling cannot be applied directly to the data
without a pre-processing step. In this paper we use a machine learning method
to learn the relationship between pairs of data points at different time
separations. The input vector comprises a summary of the time series history
and includes both demographic and non-time varying variables such as genetic
data. The dataset used is from the 2017 TADPOLE grand challenge which aims to
predict the onset of Alzheimer’s disease using including demographic, physical
and cognitive data. The challenge is a three-fold diagnosis classification
into AD, MCI and control groups, the prediction of ADAS-13 score and the
normalised ventricle volume. While the competition proceeds, forecasting
methods may be compared using a leaderboard dataset selected from the
Alzheimer’s Disease Neuroimaging Initiative (ADNI) and with standard metrics
for measuring accuracy. For diagnosis, we find an mAUC of 0.82, and a
classification accuracy of 0.73. The results show that the method is effective
and comparable with other methods.

###### keywords:

Alzheimer’s disease; Mild cognitive impairment; Machine learning; ADNI;
TADPOLE; DPUK;

††journal: Alzheimer’s and Dementia

##  1 Introduction

Alzheimer’s disease (AD) is an irreversible brain disorder which progressively
affects cognition and behaviour, and results in an impairment in the ability
to perform daily activities. It is the most common form of dementia in older
people, affecting about 6% of the population aged over 65, and it increases in
incidence with age. The initial stage of AD is characterised by memory loss,
and this is the usual presenting symptom. Memory loss is one constituent of
mild cognitive impairment (MCI), which can be an early sign of Alzheimer’s
disease. MCI is diagnosed by complaints of subjective memory loss (preferably
corroborated by a close associate or partner of the individual), impairment of
memory function, unimpaired general cognition and behaviour but with no
evidence of dementia [1]. MCI does not always progress to dementia or to a
diagnosis of Alzheimer’s disease, but those with amnestic mild MCI, the type
of MCI characterised by memory impairment, are more likely to develop dementia
than those without this diagnosis. In cases where an individual does develop
Alzheimer’s disease, the phase of MCI ends with a marked decline in cognitive
function, lasting two to five years, in which semantic memory (the recall of
facts and general knowledge) and implicit memory (the long-term, nonconscious
memory evidenced by priming effects) also becomes degraded.
Clinical diagnosis of dementia relies on information from a close associate or
partner of the individual, and on cognitive and physical examinations. Once
dementia is diagnosed it is usually subclassified into Alzheimer’s disease,
vascular dementia or Lewy Body dementia [2][3], these three classes making up
the majority of cases. Risk factors for Alzheimer’s disease are multifarious,
including sociodemographic (in particular age), genetic (notably ApoE status),
and medical history (such as a diagnosis of depression). The cause of
Alzheimer’s disease is not fully understood, but plaques containing amyloid
$\beta$–peptide (A$\beta$) in brain tissue and neurofibrillary tangles
containing tau protein are the primary histological features[4].

###  1.1 Predicting Alzheimer’s disease

The disease pathology leads to an progressive, irreversible loss of brain
function which suggests that prospective drug therapies should be tested for
efficacy as early in the process as possible. So there has been a demand for
predicting which individuals will develop AD as early as possible in order to
test drug therapies which might inhibit or prevent tissue damage. There has
been much research effort put into the prediction of an AD diagnosis among
those who are diagnosed with MCI, in particular using imaging to detect early
signs of the disease pathology: a meta analysis of 32 structural MRI or
amyloid PET imaging studies that reported conversion to AD in patients with
MCI is given by Seo _et al._[5]. This analysis concluded that amyloid PET is a
better predictor of progression to AD from MCI than MRI atrophy measures
(effect size 1.32 vs 0.77), but that MRI on entorhinal cortex atrophy (effect
size 1.26) is comparable in prediction value to that of amyloid PET. Another
comparison of biomarker predictivity found that the highest predictive
accuracy was achieved by combinations of amyloidosis and neurodegeneration
biomarkers [6]. The individual biomarker with the best performance was
[18F]-fluorodeoxyglucose-positron emission tomography (FDG-PET) which measures
temporoparietal hypometabolism.
Cognitive markers have also been widely applied for early detection of
Alzheimer’s disease: a review is presented by Gainotti _et al._ in [7] which
concluded that measures of delayed recall are the best neuropsychological
markers of conversion from MCI to AD. Significantly, they also suggest that
MCI subjects with deficits in multiple cognitive domains including memory may
not be the best candidates for clinical trials of disease-modifying drugs: of
this group about 50% of this will convert to AD within 2 years, making their
condition less modifiable than for those who are at an earlier stage of the
disease.

###  1.2 The TADPOLE challenge

In evaluating a method for predicting Alzheimer’s disease it is important to
compare the results with the current state of the art in order to calibrate
the accuracy. In the past few years there have been a number of challenges
which allow comparison between methods using a common data set and
standardised evaluation metrics. The CADDementia challenge [8] compares
algorithms for multi-class classification of AD, MCI and controls based on
structural MRI data. The Kaggle Neuroimaging challenge
https://www.kaggle.com/c/mci-prediction [9] is based on the Kaggle machine
learning platform and uses data from the Alzheimer’s Disease Neuroimaging
Initiative (ADNI) http://adni.loni.usc.edu/ which is one of the most commonly
used data sets for studies of Alzheimer’s disease[10]. The challenge involved
a four-fold classification into AD, MCI, MCI converters to AD, and controls.
The 2017 TADPOLE grand challenge https://tadpole.grand-challenge.org/ is
currently taking place with the evaluation to be completed by January 2019.
The challenge is a three-fold diagnosis classification into AD, MCI and
control groups, and the prediction of ADAS-13 score and normalised brain
volume [11]. The TADPOLE challenge has the aim of predicting the onset of
Alzheimer’s disease using different modes of measurement, including
demographic, physical and cognitive data. In common with many other
studies[10], the TADPOLE data set is also derived from ADNI. ADNI itself is
comprised of four phases: ADNI-1 (2004), ADNI-GO (2009), ADNI-2 (2011), and
ADNI-3 (2016). ADNI-1 registered 200 healthy elderly, 400 participants with
MCI, and 200 participants with AD, and the subsequent phases continued to add
participants. The TADPOLE competition involves predicting future data
collected as part of the ADNI-3 phase. The competition organisers provide a
leaderboard dataset which is separate from the main competition and which
allows prediction methods from different teams to be evaluated. The results
presented here are derived from the TADPOLE leaderboard dataset. Since TADPOLE
data is based on ADNI, data used in the preparation of this article were
obtained from the (ADNI) database (adni.loni.usc.edu). ADNI is led by
Principal Investigator Michael W. Weiner, MD. For up-to-date information see
www.adni-info.org.

##  2 Forecasting

###  2.1 Leaderboard data

The leaderboard dataset has a training set LB1 and a set LB2 whose
participants subsequently continued from ADNI-1 into ADNI GO/ADNI-2 to form
the leaderboard test set LB4. LB2 is formed of ADNI-1 time points for 110
participants who who were not diagnosed with AD at the last ADNI-1 time point.
The test set LB4 comprises the data points for those same LB2 participants
during their continuing participation in ADNI GO/ADNI-2. The training set LB1
comprises data from participants who are not represented in LB2. The task is
to predict the diagnosis, ADAS-13 score and the normalised ventricle volume
for the set LB4 using set LB1 and the participant histories recorded in LB2.
The results are evaluated by comparison with LB4 data using a variety of
metrics. No information from LB4 may be used for model training, but
demographic and other details about the participants who contributed to LB4
are available from LB2, and past time varying data such as imaging and
cognitive measurements are also available from LB2. A histogram of time series
lengths for LB1 and LB2 is shown in Figure 1.

Figure 1: Histograms of time series lengths. Upper: training set LB1 whose
time series may cover ADNI, ADNI-GO and ADNI-2. Lower: Set LB2 which is formed
only from time series in from ADNI-1.

Features for prediction are selected from the demographic, cognitive and
physical data variables in the ADNI/TADPOLE data. The physical data comprises,
among other measurements, MRI data (volumes, cortical thickness, surface
area), PET (FDG, AV45 and AV1451), DTI (regional means of standard indices)
and levels of markers from cerebral spinal fluid (CSF).

###  2.2 Evaluation set

For the purposes of training we form an evaluation set which is similar to the
time series used in the leaderboard evaluation, that is LB2 from the ADNI-1
phase and the test set LB4 from the ADNI-GO and ADNI-2 phases. We select the
evaluation set from LB1 by choosing participants who match those of LB2 and
whose ADNI-1 time series length is similar. The post-ADNI-1 phases of this
matched evaluation set can be used to assess the prediction accuracy, which
should be similar to that of the test set LB4. To create the evaluation set we
examine each participant time series in LB2 and find those participants in LB1
who have a matching gender, ApoE status and age (to within 5 years) and whose
diagnosis matches at the start and end of the ADNI-1 period. If more than one
matching participant is found we select the one who has the closest match for
the time series length in the ADNI-1 phase. The demographic characteristics
and ApoE status of the participants from set LB2 and the matched evaluation
set are shown in Figure 1.

|  LB2 |  Matched set
---|---|---
n: |  110 |  92
|  |
Age: |  59.9 (75.1) 87.9 |  57.8 (75.3) 84.8
|  |
Male: |  60.9% |  60.9%
Female: |  39.1% |  39.1%
|  |
APOE 0: |  70.0% |  68.5%
APOE 1: |  27.3% |  29.4%
APOE 2: |  2.7% |  2.2%
Table 1: Demographic characteristics and ApoE status for participants from the
set LB2 compared with a matched evaluation set selected from LB1. The
variables shown are the sample size $n$, age as minimum, mean and maximum,
gender and ApoE status.

###  2.3 Training

We train the model using the time series from LB1 and LB2. Points from ADNI-GO
and ADNI-2 which are used to compute prediction accuracy are not used for for
training. Training is performed on 90% of the participants in the evaluation
set with accuracy measured on the remaining 10%, this repeated for 10
independent splits of the whole evaluation set. We train only on time series
with at least 4 points, this minimum having been determined during training.
The prediction variables are selected manually by optimising the mean accuracy
found on the evaluation set.

###  2.4 Forecasting method

The purpose of a forecasting method is to predict a patient’s condition at
points in the future using demographic, cognitive and physical data variables
from time points in the participant’s history. A common approach to automatic
prediction is to use time series methods which use weighted combinations of
past data points to predict the next data point. Time series models in general
encode a mapping from an $r$-dimensional space to the output, where time is
not one of the input dimensions. But many time series in the training data are
short and the sampling periods are irregular, so much of the information in
the training set lies in the mapping from the time delay between measurements
to the output rather than in the sequence of input values555Irregular sampling
and missing data can be managed by interpolation or by using appropriate
methods such as Gaussian process regression [12], but these approaches entail
making assumptions about the distributions.. Another approach is to use an
input space formed of demographic variables $\lambda$, last diagnosis
$g_{(t-\Delta t)}$, time since last measurement $\Delta t$, and map vectors in
this to the output variable $g_{t}$. Again assuming additive error, the model
is,

$g_{t}=f(\lambda,\,g_{(t-\Delta t)}\,,\Delta_{t})+\epsilon_{t}$ (1)

We use an ensemble of decision trees to estimate the regression function $f$.
Decision trees approximate the regression function by partitioning the input
(feature) space into a set of rectangles [13, p305]. The training algorithm
iterates over all the features and selects the feature and split point that
gives the best partition for the training data; this is repeated until a
stopping criterion is met, such as a minimum number of points in the
rectangle. The best partition is that that which gives the minimum total
impurity in the two subsets that are formed. However, in our experience
decision trees own tend to overfit the training data and perform poorly on new
data, so we use a ensemble of trees and poll the individual results as an
estimator. Further improvement is seen with the random forest algorithm in
which the features are chosen randomly at each split point [14]. An
introduction to the theory of random forests is given in Hastie _et al._[13,
ch16].

##  3 Results

There are three target outcomes for prediction: 1) Diagnosis, 2) the ADAS-13
score, and 3) VENTS-ICV which is the ventricles volume divided by intracranial
volume. We first present results from the evaluation set, followed by the test
set accuracy.

###  3.1 Evaluation set

#### Diagnosis

The accuracy for ten independent splits of 10% of the evaluation set, and the
training error on the full evaluation set is shown in Table 2.

| Acc(baseline) | Acc | mAUC | BCA
---|---|---|---|---
_Split:_ | 61.54 | 69.23 | 0.87 | 0.75
| 73.53 | 73.53 | 0.77 | 0.64
| 69.57 | 69.57 | 0.73 | 0.44
| 52.38 | 52.38 | 0.74 | 0.59
| 86.49 | 86.49 | 0.83 | 0.78
| 73.68 | 86.84 | 0.99 | 0.93
| 70.21 | 74.47 | 0.85 | 0.78
| 62.50 | 78.13 | 0.73 | 0.69
| 91.43 | 91.43 | 0.76 | 0.78
| 88.64 | 88.64 | 0.90 | 0.78
|  |  |  |
Mean: | 73.00 | 77.07 | 0.82 | 0.71
Full: | 73.25 | 76.50 | 0.85 | 0.77
Table 2: Prediction accuracy for diagnosis in the evaluation set. The first
ten rows show the results for each partition of the evaluation set. The final
row labelled _Full_ shows the training accuracy for the entire set of 92
participants. The first column shows a baseline accuracy which is obtained by
using the last diagnosis as the predictor for subsequent values. The metrics
used are taken from the TADPOLE competition and the codes reimplemented in
order to double-check the results. As a measure of accuracy we report the
multiclass area under the receiver operating curve (mAUC) and balanced
classification accuracy (BCA). The mAUC is based on Hand and Till’s extension
of AUC to multiple classes [15] which takes the average AUC over all the pairs
of classes, where each pair of AUCs
$\hat{A}(c_{i},c_{j}),\hat{A}(c_{j},c_{i})$ is itself averaged. The balanced
classification accuracy (BCA) is based on point scores, and is the mean of the
True Positive rate and True Negative rate.

#### ADAS-13 and VENTS-ICV

The prediction error for ten independent splits of 10% of the evaluation set,
and the training error on the full evaluation set is shown in Table 3 where
the first two columns show ADAS-13 results and the next two columns show those
for the ratio of ventricle volume divided by intracranial volume.

| _ADAS-13_ | _VENTS-ICV_
---|---|---
| MAE(baseline) | MAE | MAE(baseline) | MAE
_Split:_ | 9.16 | 6.18 | 0.0034 | 0.0011
| 6.28 | 5.18 | 0.0027 | 0.0036
| 5.11 | 5.15 | 0.0033 | 0.0017
| 8.15 | 6.39 | 0.0037 | 0.0020
| 5.06 | 4.43 | 0.0028 | 0.0017
| 8.10 | 5.80 | 0.0041 | 0.0013
| 8.76 | 6.05 | 0.0048 | 0.0026
| 7.55 | 5.29 | 0.0027 | 0.0040
| 4.27 | 5.61 | 0.0042 | 0.0022
| 7.50 | 5.50 | 0.0023 | 0.0011
|  |  |  |
Mean: | 6.99 | 5.56 | 0.0034 | 0.0021
Full: | 6.97 | 5.71 | 0.0035 | 0.0021
Table 3: Mean absolute error for predicting ADAS-13 and VENTS-ICV in the
evaluation set. In each case the baseline is a prediction using the last value
of the variable to be predicted. The first ten rows show the results for each
partition of the evaluation set. The final row labelled _Full_ shows the
result for the entire set of 92 participants.

#### Predictors

The predictor variables that were selected during training are shown in Table
4. These were chosen by starting from a base set of variables and adding
variables to increase the prediction accuracy. The set of predictors for
diagnosis and ADAS-13 are the same except that for ADAS-13 the most recent
value of the variable ADAS13 and its slope are added.

Variable | Meaning
---|---
RID | Participant identifier
TIME_DELAY | Number of months delay
DX | Diagnosis (NL or MCI or AD)
AGE | Age
PTGENDER | Gender
ApoE | ApoE allele
FUSIFORM_BL | Fusiform volume at baseline
MMSE | MMSE Mini-mental state examination
CDRSB | CDRSB
FAQ | Functional activities questionnaire
$\Delta$VENTRICLES | Ventricles volume slope
$\Delta$HIPPOCAMPUS | Hippocampus volume slope
$\Delta$MMSE | MMSE slope
Table 4: The set of variables from which features are chosen for predicting
diagnosis and ADAS-13 values. The most recent value of each variable is used
for prediction. The MMSE value is thresholded at 26. For predicting ADAS-13,
the variables ADAS13 and $\Delta$ADAS13 are added. For predicting VENTS-ICV,
the two target variables VENTS and ICV are predicted separately using the last
value and slope of the respective variable, with TIME_DELAY also used. The
prefix $\Delta$ indicates that the slope of the variable over the history is
used for prediction.

###  3.2 Test set LB4

The accuracy on the test set LB4 is shown as the highlighted row of Table 6
which reproduces the results from the TADPOLE competition leaderboard table.
The leaderboard shows entries in rank order where the rank is determined by
the lowest sum of individual ranks for mAUC, ADAS-13 MAE and VENTS-ICV MAE.
For diagnosis the accuracy is mAUC=0.82 and BCA=0.73, which compares a mean
accuracy on our evaluation set of mAUC=0.82 and BCA=0.71. The similarity of
test and evaluation errors shows that the evaluation set is well matched to
the test set and that the model has not been overtrained. For ADAS-13
prediction the test set error is MAE=5.19, and the evaluation set error is
MAE=5.56 and for VENTS-ICV the test error is MAE=0.0023 and the evaluation
error is MAE=0.0021. The confusion matrix for the test set is shown in Table
5.

|  | _Predicted diagnosis_
---|---|---
|  | NL | MCI | AD
_Actual diagnosis:_ |  NL | 193 | 2 | 0
MCI | 54 | 88 | 8
AD | 6 | 45 | 21
Table 5: Confusion matrix for predicting the diagnosis of the test set. In this case, the a point forecast is derived from the probabilistic forecast by selecting the diagnosis with the highest score. Diagnosis | ADAS-13 | VENTS-ICV
---|---|---
mAUC |  BCA |  MAE |  WES |  CPA |  MAE |  WES |  CPA
0.91 |  0.83 |  3.62 |  3.62 |  0.11 |  0.0020 |  0.0018 |  0.13
0.93 |  0.85 |  3.72 |  3.10 |  0.02 |  0.0020 |  0.0016 |  0.15
0.93 |  0.85 |  3.72 |  3.10 |  0.02 |  0.0020 |  0.0016 |  0.15
0.91 |  0.83 |  3.67 |  3.67 |  0.12 |  0.0024 |  0.0022 |  0.08
0.91 |  0.74 |  3.73 |  3.70 |  0.01 |  0.0028 |  0.0023 |  0.32
0.89 |  0.78 |  4.16 |  4.16 |  0.39 |  0.0023 |  0.0023 |  0.47
0.89 |  0.82 |  3.76 |  3.76 |  0.12 |  0.0034 |  0.0029 |  0.15
0.89 |  0.82 |  3.80 |  3.80 |  0.11 |  0.0034 |  0.0029 |  0.14
0.87 |  0.78 |  4.12 |  4.08 |  0.03 |  0.0027 |  0.0027 |  0.01
0.87 |  0.69 |  4.41 |  4.41 |  0.30 |  0.0026 |  0.0026 |  0.46
0.84 |  0.74 |  4.54 |  4.17 |  0.49 |  0.0025 |  0.0021 |  0.49
0.89 |  0.81 |  3.81 |  3.81 |  0.11 |  0.0057 |  0.0041 |  0.01
0.88 |  0.80 |  3.87 |  3.87 |  0.11 |  0.0049 |  0.0038 |  0.05
0.91 |  0.74 |  3.73 |  3.70 |  0.01 |  0.0092 |  0.0092 |  0.01
0.80 |  0.74 |  4.51 |  4.49 |  0.40 |  0.0027 |  0.0027 |  0.25
0.82 |  0.73 |  5.19 |  4.57 |  0.07 |  0.0023 |  0.0019 |  0.11
0.76 |  0.67 |  4.34 |  4.30 |  0.08 |  0.0022 |  0.0021 |  0.08
0.88 |  0.80 |  5.00 |  4.78 |  0.03 |  0.0030 |  0.0030 |  0.05
0.88 |  0.80 |  3.92 |  3.92 |  0.10 |  0.0060 |  0.0043 |  0.01
0.86 |  0.70 |  4.56 |  3.69 |  0.14 |  0.0034 |  0.0032 |  0.43
0.81 |  0.73 |  5.13 |  5.14 |  0.01 |  0.0027 |  0.0028 |  0.20
0.81 |  0.73 |  4.09 |  4.09 |  0.09 |  0.0045 |  0.0038 |  0.01
0.80 |  0.74 |  4.51 |  4.49 |  0.40 |  0.0038 |  0.0038 |  0.42
0.80 |  0.68 |  4.14 |  4.14 |  0.29 |  0.0040 |  0.0040 |  0.38
0.80 |  0.66 |  4.81 |  4.81 |  0.21 |  0.0038 |  0.0038 |  0.10
0.80 |  0.74 |  4.60 |  4.60 |  0.35 |  0.0041 |  0.0041 |  0.12
0.88 |  0.69 |  4.98 |  4.98 |  0.34 |  0.0066 |  0.0066 |  0.27
0.78 |  0.71 |  4.60 |  4.60 |  0.35 |  0.0041 |  0.0041 |  0.12
0.79 |  0.69 |  6.68 |  5.54 |  0.05 |  0.0028 |  0.0023 |  0.32
0.81 |  0.72 |  4.70 |  4.70 |  0.09 |  0.0070 |  0.0070 |  0.03
0.77 |  0.65 |  4.83 |  4.83 |  0.20 |  0.0038 |  0.0038 |  0.07
0.87 |  0.70 |  4.91 |  4.79 |  0.36 |  0.0073 |  0.0073 |  0.46
0.77 |  0.68 |  5.85 |  5.85 |  0.38 |  0.0032 |  0.0032 |  0.34
0.71 |  0.63 |  6.37 |  6.71 |  0.39 |  0.0026 |  0.0026 |  0.32
0.71 |  0.63 |  6.37 |  6.74 |  0.25 |  0.0026 |  0.0026 |  0.27
0.79 |  0.66 |  4.69 |  4.69 |  0.09 |  0.0093 |  0.0093 |  0.01
0.76 |  0.69 |  5.00 |  4.98 |  0.35 |  0.0042 |  0.0042 |  0.38
0.72 |  0.62 |  5.70 |  5.70 |  0.41 |  0.0036 |  0.0036 |  0.43
0.73 |  0.59 |  9.63 |  9.63 |  0.45 |  0.0029 |  0.0029 |  0.48
0.80 |  0.68 |  6.00 |  6.00 |  0.11 |  0.0075 |  0.0075 |  0.17
0.71 |  0.58 |  9.70 |  9.70 |  0.40 |  0.0029 |  0.0029 |  0.26
0.74 |  0.68 |  5.70 |  4.60 |  0.21 |  0.0070 |  0.0042 |  0.35
0.74 |  0.68 |  5.70 |  4.60 |  0.21 |  0.0070 |  0.0042 |  0.35
0.77 |  0.65 |  6.73 |  6.73 |  0.13 |  0.0094 |  0.0094 |  0.02
0.78 |  0.68 |  7.39 |  7.39 |  0.12 |  0.0095 |  0.0095 |  0.04
0.78 |  0.66 |  8.43 |  5.09 |  0.48 |  0.0096 |  0.0095 |  0.50
Table 6: Competition leaderboard table at 4 May 2018 where each row represents
an entry from a competition team and our entry is highlighted. There are three
target outcomes for prediction: 1) Diagnosis, 2) the ADAS-13 score, and 3)
VENTS-ICV which is the ventricles volume divided by intracranial volume.
Predictions for diagnosis are presented as relative probabilities for each of
the three potential diagnostic categories. For the ADAS score, and the
normalised ventricles volume, we provide confidence intervals which indicate
in the limit where 50% of the predictions would lie if an experiment were
repeated many times on new data. The rank is determined by the lowest sum of
ranks from mAUC, ADAS-13 MAE and VENTS-ICV MAE. The metrics are based on those
used in the TADPOLE competition. For diagnosis classification we use the
multiclass area under the receiver operating curve (mAUC) and balanced
classification accuracy (BCA) as described in Table 2. The metrics used for
ADAS-13 and VENTS-ICV are the mean absolute error (MAE), the weighted error
score (WES), which is the absolute error weighted by the inverse of the
confidence interval range, and the coverage probability accuracy (CPA),
defined as, $CPA=|j-0.5|$, where $j$ is the proportion of measurements falling
within the 50% confidence interval.

##  4 Discussion

In selecting participants for clinical trials, a positive PET scan is commonly
used as part of the inclusion criteria. However PET imaging is expensive, so
when a positive scan is one of the trial inclusion criteria it is desirable to
avoid screening failures. So one application of predicting Alzheimer’s disease
is to preselect candidates before applying the criteria. Time series collected
both in clinic and from studies such as ADNI inevitably have missing data
points, and are of variable length. The same will be true for clinical data
collected from patients, since it is not uncommon for appointments to be
missed, and for people to withdraw from data collection for various reasons.
Most time series prediction methods assume data which is complete and
regularly sampled, so that it has to be pre-processed using imputation or
interpolation methods to fulfil this assumption. In this paper, rather than
using a traditional time series method we have used a machine learning method
to learn the relationship between pairs of time points at different
separations. The input vector comprises a summary of the time series history
up to that point and the demographic and non-time varying factors such as
genetic data. This method makes no assumptions about the dynamics of the time
series, and it is applicable to data which has missing and irregularly sampled
points. The results are better than a baseline last-value estimator, and they
validate the method as effective.

##  5 Acknowledgements

Data collection and sharing for this project was funded by the Alzheimer’s
Disease Neuroimaging Initiative (ADNI) (National Institutes of Health Grant
U01 AG024904) and DOD ADNI (Department of Defense award number
W81XWH-12-2-0012). A full list of funding sources for ADNI is provided in the
document ‘Alzheimer’s Disease Neuroimaging Initiative (ADNI) Data Sharing and
Publication Policy’ available through adni.loni.usc.edu/.
This work uses the TADPOLE data sets https://tadpole.grand-challenge.org
constructed by the EuroPOND consortium http://europond.eu funded by the
European Union’s Horizon 2020 research and innovation programme under grant
agreement No 666992.
The MRC Dementias Platform UK (DPUK) https://www.dementiasplatform.uk/
provided support in the preparation of this paper. DPUK is a multi-million
pound public-private partnership, developed and led by the MRC, to accelerate
progress in and open up dementias research. The aims of DPUK are early
detection, improved treatment and ultimately the prevention of dementias.

##

## References

  * [1] P. J. Nestor, P. Scheltens, J. R. Hodges, Advances in the early detection of Alzheimer’s disease, Nature medicine 10 (7) (2004) S34.
  * [2] A. Burns, S. Iliffe, Alzheimer’s disease, https://doi.org/10.1136/bmj.b158, [Online; accessed 20 September 2017].
  * [3] B. Dubois, H. H. Feldman, C. Jacova, S. T. DeKosky, P. Barberger-Gateau, J. Cummings, A. Delacourte, D. Galasko, S. Gauthier, G. Jicha, et al., Research criteria for the diagnosis of alzheimer’s disease: revising the NINCDS–ADRDA criteria, The Lancet Neurology 6 (8) (2007) 734–746.
  * [4] P. Tiraboschi, L. Hansen, L. Thal, J. Corey-Bloom, The importance of neuritic plaques and tangles to the development and evolution of AD, Neurology 62 (11) (2004) 1984–1989.
  * [5] E. H. Seo, W. Y. Park, I. Choo, Structural MRI and Amyloid PET Imaging for Prediction of Conversion to Alzheimer’s Disease in Patients with Mild Cognitive Impairment: A Meta-Analysis, Psychiatry investigation 14 (2) (2017) 205–215.
  * [6] A. Prestia, A. Caroli, S. K. Wade, W. M. Van Der Flier, R. Ossenkoppele, B. Van Berckel, F. Barkhof, C. E. Teunissen, A. Wall, S. F. Carter, et al., Prediction of AD dementia by biomarkers following the NIA-AA and IWG diagnostic criteria in MCI patients from three European memory clinics, Alzheimer’s & Dementia 11 (10) (2015) 1191–1201.
  * [7] G. Gainotti, D. Quaranta, M. G. Vita, C. Marra, Neuropsychological predictors of conversion from mild cognitive impairment to Alzheimer’s disease, Journal of Alzheimer’s Disease 38 (3) (2014) 481–495.
  * [8] E. E. Bron, M. Smits, W. M. Van Der Flier, H. Vrenken, F. Barkhof, P. Scheltens, J. M. Papma, R. M. Steketee, C. M. Orellana, R. Meijboom, et al., Standardized evaluation of algorithms for computer-aided diagnosis of dementia based on structural MRI: the CADDementia challenge, NeuroImage 111 (2015) 562–579.
  * [9] A. Sarica, A. Cerasa, A. Quattrone, V. Calhoun, Editorial on Special Issue: Machine learning on MCI (2018).
  * [10] M. W. Weiner, D. P. Veitch, P. S. Aisen, L. A. Beckett, N. J. Cairns, R. C. Green, D. Harvey, C. R. Jack, W. Jagust, J. C. Morris, et al., Recent publications from the Alzheimer’s Disease Neuroimaging Initiative: Reviewing progress toward improved AD clinical trials, Alzheimer’s & Dementia.
  * [11] R. V. Marinescu, N. P. Oxtoby, A. L. Young, E. E. Bron, A. W. Toga, M. W. Weiner, F. Barkhof, N. C. Fox, S. Klein, D. C. Alexander, EuroPOND Consortium., TADPOLE Challenge: Prediction of Longitudinal Evolution in Alzheimer’s Disease, ArXiv e-printsarXiv:1805.03909.
  * [12] C. E. Rasmussen, C. K. Williams, Gaussian processes for machine learning, Vol. 1, MIT press Cambridge, 2006.
  * [13] T. Hastie, R. Tibshirani, J. Friedman, T. Hastie, J. Friedman, R. Tibshirani, The elements of statistical learning, Vol. 2, Springer, 2009.
  * [14] L. Breiman, Random forests, Machine learning 45 (1) (2001) 5–32.
  * [15] D. J. Hand, R. J. Till, A simple generalisation of the area under the ROC curve for multiple class classification problems, Machine learning 45 (2) (2001) 171–186.


1Chair of Embedded Intelligence for Health Care and Wellbeing, University of
Augsburg, Germany
2GLAM – Group on Language, Audio, & Music, Imperial College, UK
3Department of Cardiology, Respiratory Medicine and Intensive Care, University
Hospital Augsburg, University of Augsburg, Germany
4Ludwig-Maximilians-University Munich, Germany

#  Distinguishing between pre- and post-treatment in the speech of
patients with chronic obstructive pulmonary disease

###### Abstract

Chronic obstructive pulmonary disease (COPD) causes lung inflammation and
airflow blockage leading to a variety of respiratory symptoms; it is also a
leading cause of death and affects millions of individuals around the world.
Patients often require treatment and hospitalisation, while no cure is
currently available. As COPD predominantly affects the respiratory system,
speech and non-linguistic vocalisations present a major avenue for measuring
the effect of treatment. In this work, we present results on a new COPD
dataset of 20 patients, showing that, by employing personalisation through
speaker-level feature normalisation, we can distinguish between pre- and post-
treatment speech with an unweighted average recall (UAR) of up to 82 % in
(nested) leave-one-speaker-out cross-validation. We further identify the most
important features and link them to pathological voice properties, thus
enabling an auditory interpretation of treatment effects. Monitoring tools
based on such approaches may help objectivise the clinical status of COPD
patients and facilitate personalised treatment plans.

Index Terms: digital health, pathological speech, COPD, personalisation,
feature interpretation

##  1 Introduction and related work

Chronic obstructive pulmonary disease (COPD) is a respiratory disease
characterised by a chronically inflamed and obstructed airway. The long-term
exposure to damaging irritants, especially cigarette smoke, is the predominant
cause of COPD [1] – the third leading cause of death after ischemic heart
disease and stroke [2]. Its prevalence in Europe ranges between 15 and 20 %
for adults aged over 40 years [3]. Thus, the socio-economic burden of COPD is
immense and results in a high consumption of clinical resources and overall
costs to society [4]. While the clinical appearance of COPD varies, the main
symptoms are chronic and progressive dyspnea, as well as coughing. Sometimes,
patients suffer from a severe deterioration of their respiratory symptoms,
called exacerbation, which leads to a need of intensified therapy, often under
in-patient or even intensive care treatment. Besides treatment and prevention
of exacerbation, the main objective of COPD therapy is to provide symptomatic
relief. For this purpose, patients receive (mainly inhalative) medication,
such as inhaled corticosteroids (ICS), long-acting muscarinic antagonists
(LAMA) or long-acting beta-2-agonists (LABA) – often administered in
combination. Sometimes, further systemic medication, such as systemic
corticosteroids, is needed. The intensity of treatment depends on the severity
of COPD, which is classified according to the recommendations of the Global
Initiative of Chronic Obstructive Lung Disease. This classification is based
on the severity of airflow limitations and takes into account symptoms and
risks of exacerbation [5]. Spirometric examinations and clinical findings are
still the relevant diagnostic tools for COPD. Especially for acute
exacerbation, clinical practitioners must rely on clinical examination to
monitor treatment success or failure. So far, there are no technical tools to
objectivise clinical symptoms of COPD, especially during an exacerbation
episode. In order to accelerate diagnosis and distinguish different
respiratory illnesses, new artificial intelligence (AI)-assisted monitoring
tools can be helpful. For instance, new data shows the potential use of AI
speech analysis for respiratory diseases, such as COVID-19 [6]. It is
intuitive to expand these findings to COPD, since this obstructive airway
disease inevitably affects speech and non-linguistic vocalisations, especially
during exacerbation.

Due to the widespread prevalence of COPD and its negative effect on public
health, voice-based digital detection and monitoring tools have recently
attracted increased attention [7, 8, 9, 10, 11, 12, 13]. These utilise
different types of vocalisations, such as breathing [10], coughing [8],
sustained vowels [11], or read/free speech [7, 12, 11] to distinguish between
COPD patients and healthy individuals and different states of COPD (such as
‘stable’ vs exacerbation [11]). Yet, most of these studies are merely
identifying acoustic descriptors that are correlated with COPD and do not
build an automatic detection tool. Instead, we focus on developing a machine
learning (ML)-based voice evaluation tool that distinguishes between pre- and
post-treatment states of patients after exacerbation, based on read speech. We
investigate a set of different feature sets, segmentation strategies, and
normalisation procedures. It turns out that speaker-level feature
normalisation is crucial for obtaining good performance – demonstrating that
personalisation is key for this application. This paves the way for more
advanced personalisation techniques which adapt to specific speakers using
either speaker-dependent models [14] or test-time adaptation [15].
Furthermore, we try to interpret the most important features, which helps
characterise the effect of exacerbation and the corresponding benefits of
treatment on the speakers’ voice.

The remainder of our contribution is organised as follows: Section 2 describes
the dataset used in this study. Section 3 outlines our experimental protocol,
followed by our results and accompanying discussion and interpretation in
Section 4. The work ends with some concluding remarks in Section 5.

##  2 Dataset

Our COPD dataset was recorded at the University Hospital Augsburg between
October 2020 and December 2021. Patients were recruited soon after
hospitalisation, if possible, already in the emergency department or the
intensive care unit. Only patients older than 18 years, able to sit and read a
short text without any need of ventilation during the time of recording, were
included, resulting in: 20 (11 male / 9 female) subjects, aged 48 to 82
(median: 70), with a median of 37.5 pack years111Pack years are calculated by
multiplying the number of packs of cigarettes smoked per day by the number of
years the person has smoked. and an improvement (post- to pre-treatment)
between 0 and 7 (median: $2.39$) on a modified Borg scale, a subjective
assessment of dyspnea from 0 (worst) to 10 (best).

The local ethics committee approved the study on June 24, 2020 (BKF 2020-34).
Two recordings – one pre-treatment, one post-treatment – with a distance of 1
to 16 days (median: 5) took place bedside with the portable recorder H5 from
Zoom® and a Sony lapel mic ECM-144. All patients obtained their standard and
individual home medication, mainly LABA and LAMA, sometimes in addition to ICS
and systemic corticosteroids. Some patients needed non-invasive ventilation,
which was paused for the time of recording.

Patients were required to produce:  a) a set of sustained vowels (/a:/, /e:/,
/i:/, /o:/, /u:/);  b) a few spontaneous utterances;  c) (forced) coughing;
d) breathing;  e) reading Der Nordwind und die Sonne [The Northwind and the
Sun] (NuS).  We assume no or a negligible habituation effect, as the second
recording took place days after the first one. Here, we deal only with NuS: it
is longer than other sound types (median: 53 s), thus, resulting in more
samples after segmentation, which is beneficial for ML algorithms. This was
confirmed by preliminary experiments with the other sounds.

##  3 Experimental setup

Segmentation: the North Wind and the Sun [Der Nordwind und die Sonne] (NuS) is
too long as a unit of analysis for most speech processing applications, which
typically operate on shorter segments. For a segmentation yielding shorter
units, we use the Munich AUtomatic Segmentation (MAUS) system [16, 17]. It
utilises forced alignment to derive word and phone boundaries from the text
transcriptions, which in the case of read speech is trivially available. We
experiment with two different types of segmentation resulting in two different
units of analysis: Word units, where we keep the original word boundaries
returned by MAUS, resulting in a total of $18\times 2\times 188=3888$
segments; and Phrase units, where we segmented the story into $20$ prosodic
phrases for a total of $18\times 2\times 20=720$ segments.

Features: We extract a set of acoustic descriptors per unit (for both words
and phrases) that can be used to distinguish between pre- and post-treatment
COPD speech, employing both expert, handcrafted features, and learnt
representations of deep neural networks, thus contrasting the two dominant
ongoing trends in speech processing applications:

eGeMAPS: The extended Geneva minimalistic acoustic parameter set (eGeMAPS)
[18] is a small set of (88) interpretable acoustic parameters that has
previously been shown to contain relevant information for respiratory
diseases, such as COVID-19 [19]. eGeMAPS is extracted using openSMILE [20].

ComParE: The Interspeech Computational Paralinguistics ChallengE feature set
(ComParE) is a large-scale feature set (6373) that has been successfully used
for several computational paralinguistics tasks, beginning with the 2013
Interspeech Computational Paralinguistics Challenge [21], also extracted using
openSMILE [20].

w2v2-xlsr: Substantial progress has been seen through the use of models
trained on vast amounts of data with self-supervised methods. We use a variant
of wav2vec2.0 [22], pre-trained on 53 languages – including German [23]. The
model operates on raw audio and returns contextualised representations roughly
corresponding to 25 ms of audio with a stride of 20 ms, which we subsequently
average over the time dimension to obtain the final 1024-dimensional
embeddings.

Normalisation: We experiment with three different normalisation procedures. In
all cases, z-score normalisation on each feature is performed separately; what
changes is the set over which we compute and apply statistics.

Global: As a standard baseline, we normalise the data on a global basis – for
each fold in our cross-validation setup, we compute feature statistics on the
training set, and subsequently use those to normalise the development and
testing partitions. This is the prevailing type of normalisation.

Word/Phrase-level: We experiment with a normalisation procedure targeted at
the respective _unit of analysis_. Using read speech recordings, we collect
identical audio content for each speaker. This content, however, is influenced
by non COPD-related factors, which can be abstracted away by normalising each
word or phrase unit independently (using data from all speakers).

Speaker-level: Given our expectation that there are individual differences in
the manifestation of COPD in human vocalisations, we employ a speaker-level
normalisation procedure in an attempt to abstract away from them. This is
based on computing (and applying) mean and standard deviation normalisation
_independently_ for each speaker, that is, using all their data to compute
parameters irrespective of whether they are part of the training, development,
or test partition. As such, this form of normalisation assumes oracle
knowledge of the identity of each speaker. We consider this a realistic
assumption for personalised digital health applications in controlled
conditions.

Classifier: We use support vector machines (SVMs) where we optimise the cost
parameter ({$.0001$, $.0005$, $.001$, $.005$, $.01$, $.05$, $.1$, $.5$, $1$})
and kernel function ({linear, polynomial, radial basis function (RBF) }) in a
grid search manner. These parameters are always optimised on the development
partition.

Evaluation protocol: As the size of our dataset is limited (20 speakers), we
use leave-one-speaker-out cross-validation, whereby data from every speaker is
used exactly once for testing, each time using the data of all other speakers
for training. For each fold, we perform _nested cross-validation_ for
optimising SVM parameters by further splitting the training speakers into two
speaker-disjoint sets. Once the optimal set of parameters has been identified
(based on development set performance), we train a final model on the entire
training data for each fold.

Metrics: We use unweighted average recall (UAR), the mean of the diagonal
cells in the confusion matrix in percent. This balances the sensitivity and
specificity of both classes, which in our case are both equally important (i.
e., we have no ‘positive’ and ‘negative’ class)222As we always have the same
number of instances for both classes, UAR is identical with accuracy, as well
as with (sensitivity + specificity) / 2, and differs from F1 score throughout
just by $\pm 1$ percent.. We differentiate between three different ways of
computing UAR: unit-, story-, and speaker-level. The first (UUAR) quantifies
how well the model works over individual units (instances); the second
(STUAR), how well it classifies speakers into pre- and post-treatment states
after aggregating all individual predictions for each story (the major focus
of our work); the third (SPUAR), how well the model works for an individual
speaker by computing performance over only their instances. Given a set of
speakers $\\{s_{1},...,s_{S}\\}$ (with $S=20$ being the total number of
speakers), each producing the NuS story twice (corresponding to the two
classes {(b)efore, (a)fter}), with each story segmented into $N_{u}$ units (i.
e., words/phrases) resulting in a total of $N$ units (3888/720) overall and
$N_{s}$ units per speaker (216/40), we generate a total of $N$ unit-level
predictions $\hat{y}_{i}$ using the setup outlined above. We define the
different evaluation protocols as follows:

$\displaystyle\text{U}_{\text{UAR}}=\frac{1}{2}\sum_{c\in\\{a,b\\}}\frac{|i\in[N]:y_{i}=c,\hat{y}_{i}=c|}{|i\in[N]:y_{i}=c|}$
$\displaystyle\text{ST}_{\text{UAR}}=\frac{1}{2}\sum_{c\in\\{a,b\\}}\frac{|i\in[S]:y_{i}=c,\underset{j\in[N_{s}]}{\text{maxvote}}(\hat{y}_{j})=c|}{|i\in[S]:y_{i}=c|}$
$\displaystyle\text{SP}_{\text{UAR}}=\frac{1}{2}\sum_{c\in\\{a,b\\}}\frac{|i\in[N_{s}]:y_{i}=c,\hat{y}_{i}=c|}{|i\in[N_{s}]:y_{i}=c|}$

##  4 Results and discussion

Table 1:  UUAR and STUAR using leave-one-speaker-out cross-validation with 95
% CIs.

|  | Word units | Phrase units
---|---|---|---
Normalisation | Features | UUAR[%] | STUAR[%] | UUAR[%] | STUAR[%]
| eGeMAPS | 56 (54-57) | 60 (45-75) | 56 (52-59) | 52 (37-68)
Global | ComParE | 52 (51-54) | 60 (44-76) | 53 (49-56) | 50 (34-66)
| w2v2-xlsr | 54 (52-55) | 45 (29-61) | 59 (55-62) | 65 (50-80)
| eGeMAPS | 56 (55-58) | 60 (46-75) | 59 (56-62) | 57 (42-73)
Word/Phrase | ComParE | 53 (52-55) | 62 (47-78) | 53 (49-57) | 55 (39-70)
| w2v2-xlsr | 54 (52-55) | 50 (34-65) | 55 (51-59) | 57 (42-72)
| eGeMAPS | 60 (58-62) | 68 (53-82) | 63 (60-66) | 80 (67-92)
Speaker | ComParE | 53 (52-54) | 62 (48-79) | 55 (51-58) | 55 (40-70)
| w2v2-xlsr | 59 (58-61) | 82 (70-94) | 66 (63-70) | 78 (66-90)

Figure 1:  Average normalised feature values (taken over all utterances of a
speaker) vs SPUAR for 6 out of 10 most important features as computed by SHAP
values; values before (red, dashed, cross) and after (green, continuous,
point) treatment; identical position per speaker on the x-axis across all
plots, with crosses and points sharing the same x-coordinate corresponding to
the same speaker; thus, the rightmost points on the x-axis show the speaker
normalised mean feature values corresponding to the best performing speaker
with 98 % (39/40) of their phrases classified correctly with eGeMAPS and
speaker-level normalisation. Subtitles show STUAR (total and 95 % CI) when
using single features for classification (see text for discussion). Linear
regression lines fitted to better highlight trends.

Overall results are presented in Table 1 with UUAR and STUAR computed over all
instances and corresponding 95 % CIs computed over 1000 bootstrap samples;
STUAR shows a bigger range over UUAR, because it is computed with far less
samples (36 vs 3888/720). Story-level performance is highest for w2v2-xlsr and
word-level segmentation with a UAR of 82 % (CI: 70 %-94 %) followed by eGeMAPS
and phrase-level segmentation (STUAR: 80 %; CI: 67 %-92 %) – both using
speaker-level normalisation, with phrase-level w2v2-xlsr features trailing
close behind (STUAR: 78 %; CI: 66 %-90 %). The best result without subject-
level normalisation is obtained with ComParE with word-level segmentation and
normalisation with a STUAR of 62 % (CI: 47 %-78 %) – a large drop over
subject-level normalisation which showcases the need for personalisation.

_Interpretability_ is a necessary requirement for digital health applications
in order to explain the outcomes to patients and medical practitioners. As
eGeMAPS yields near-top performance, with the features also being easily
interpretable due to their expert-designed nature, we focus our subsequent
analysis on this setting. The 95 % CI for males (52 %-75 %) showed substantial
overlap to that of females (53 %-72 %), indicating that the classifier
performs approximately equal for both genders. We further analysed the
performance w. r. t. the available subject metadata. We first divided speakers
into two subsets: those whose individual performance exceeds the UUAR
performance of 63 % (the phrase-level UUAR for eGeMAPS when using instances
from all speakers, see Table 1), and those whose performance falls below that
threshold, and subsequently compared the 95 % CIs of the different metadata
for those two speaker groups. This comparison revealed that models work better
for subjects which have a higher post-to-pre-treatment difference in the BORG
scale ([2.12-4.75] vs [1.92-3.16]), are of a higher age ([63-73] vs [58-67]
years), and have smoked more pack years ([39-75] vs [28-44]). All these
factors might contribute to a worse clinical condition with subjects
subsequently gaining more from treatment, thus, accordingly leading to bigger
changes in their voice characteristics and making it easier to distinguish
between their pre- and post-treatment states.

We further analyse the features that have the largest impact on classifier
decisions in order to characterise the impact of treatment on patients’
voices. To that end, SHAP (SHapley Additive exPlanations) [24] has emerged as
a powerful tool for extracting feature importance values for individual
predictions. SHAP is based on Shapley values, whose theoretical definition for
each feature relies on building surrogate models on all potential feature
subsets, and taking the expectation of model output differences for all
subsets including the target features vs the same subsets but excluding that
feature [24]. These values can then be aggregated over an entire (test)
dataset to derive global feature importance values that can be used to
interpret model behaviour. We focus on the ten most important features,
defined by their average SHAP values. We computed the mean of each feature
separately (normalised using subject-level normalisation) for each subject and
phrase for pre- and post-treatment. We then plotted the resulting $18\times
2=36$ points relative to the SPUAR corresponding to each speaker. This allows
us to compare how these individual features change after treatment, but also
to relate this change to speakers for which the prediction fails. To provide a
better understanding of the effectiveness of each individual feature, we
additionally used each of them in isolation to train a (new) model with the
same experimental setup discussed before. Note that this might result in a
different ‘measure’ of feature performance as features behave differently in
isolation vs in the presence of other (potentially correlated) features [25].
In Figure 1, we show the STUAR (and 95 % CIs) obtained for each of them.

Due to space limitations, we only include 6 of those: As four of the original
ten were merely functionals of pitch (mean, median, 20th and 80th percentiles
– measured in semitones), and all of them showed a similar trend, we only
provide the best performing one, the mean. Moreover, we exclude the worst-
performing feature, the 3rd MFCC (STUAR: 60 %), showing slightly lower values
for low performing subjects.333 We know from other types of atypical speech
[26] that the vowel space is centralised, due to a less tense and less precise
articulation. This might be the case here as well. Figure 1 shows the
remaining six features.

The bandwidth of the 2nd formant F2 (STUAR: 63 %) and the bandwidth of the 3rd
formant F3 (STUAR, 68 %), above left and second left in Figure 1, are computed
from the roots of the Linear Predictor (LP) coefficient polynomial. Dysphonic
speakers display a broader formant bandwidth [27] meaning higher formant
dispersion and mutual masking of neighbouring formants and by that, vowels
[28].

Loudness (STUAR: 68 %, above right) is partially controlled by transglottal
airflow [29], which is constricted by COPD [5]; thus, patients before
treatment produce on average utterances of lower loudness; this can be seen
when we compare the declining line for before with the rising line for after
in Figure 1.444 Note that we used a lapel microphone that prevents varying
distances within the same recording session; yet, there might be slight
differences across sessions which can constitute an intervening factor that
cannot be fully controlled.

The spectral slope (STUAR: 68 %), below left in Figure 1, is computed by
fitting an OLS estimator to the logarithmic power spectrum and is thus steeper
when the higher frequencies have more energy than the lower ones. This is
opposite to the 1st MFCC (STUAR: 73 %), below middle, that can be interpreted
as the inverse spectral slope, as it is a weighted ratio of the lower to the
higher frequencies. These features show opposing trends, with the 1st MFCC
increasing and the slope decreasing after treatment – indicating that the
ratio of higher to lower frequencies decreases after treatment. A higher ratio
of higher to lower frequencies can be interpreted as higher breathiness [30],
which is then reduced through treatment. Note that higher breathiness might go
together with decreased loudness [31].

Pitch (measured in semitones, STUAR: 78 %) is the most effective power feature
[25]. It shows a strong lowering trend after treatment – in contrast to [11],
who found that F0 increases for subjects with stable COPD compared to those
with exacerbation (mean: 190 Hz vs 154 Hz). A potential confounder is that
irregular phonation caused by exacerbated COPD can lead to more errors in
pitch estimation by missing some voiced segments, especially in laryngealised
(creaky) parts [32, 33]. By default, openSMILE excludes segments with a value
of 0 in its calculation of the mean; thus, the lower pitch values post-
treatment compared to pre-treatment (mean: 150 Hz vs 160 Hz) might be due to
less irregular phonation. When including 0-valued segments in the calculation
of the mean, we obtain higher values of F0 post-treatment (mean: 89 Hz vs 85
Hz), similar to [11]. We further investigated this hypothesis by comparing the
average voiced segments per second before (mean: 24 %) and after treatment
(mean: 28 %); indeed the proportion of segments detected as voiced increases.
As the read text is identical in both conditions, (unaccounted) pitch
estimation errors remain a plausible explanation for the difference between
our findings and those of [11]. Yet, there might be a ‘cocktail’ of
intervening factors: especially before treatment, patients are more unsettled
and stressed, thus both speech pathology and psychological state might result
in strained voice and higher pitch, and at the same time, in irregular voice
partly (mis-) recognised as unvoiced. In the post-stage, speech pathology is
weakened and at the same time, the patients are relieved and more relaxed, and
all this might result in a less strained voice and lower pitch.

Summing up our interpretation: Subjects after treatment show improved
articulatory precision (as shown by the 3rd MFCC and F2/F3 bandwidth),
decreased airflow blockage (as shown by the increase in loudness), decreased
breathiness (as shown by the spectral slope and 1st MFCC), and more regular
phonation (thus less pitch errors) and, by that, lowered ‘regular’ pitch –
findings which are consistent with the expected decrease in symptomatology; as
for a comparable voice quality spectrum for Parkinson’s disease, see [34].
Naturally, although our present interpretation is consistent with previous
phonetic research and with medical expectations, it should be evaluated on a
larger sample size and tested against human evaluations.

##  5 Conclusion

We demonstrated that read passages can be successfully utilised to distinguish
between pre- and post-treatment states of COPD patients. Using a variety of
handcrafted and learnt features, we were able to achieve a top UAR of 82 % (95
% CI: 70 %-94 %) in a leave-one-speaker-out setup. Speaker-level normalisation
proved to be crucial, as it removes speaker-related effects, which prevents
generalisation; without it, performance reached a maximum of 62 %. Future work
could be directed to more data efficient personalisation techniques, which do
not require patient data to normalise with, as well as to detecting COPD in
the presence of other respiratory diseases, such as COVID-19.

##  6 Acknowledgements

This work has received funding from the DFG’s Reinhart Koselleck project No.
442218748 (AUDI0NOMOUS) and from the EU’s Horizon 2020 grant agreement No.
826506 (sustAGE).

##  7 References

## References

  * [1] T. Yoshida and RM. Tuder “Pathobiology of cigarette smoke-induced chronic obstructive pulmonary disease” In _Physiol Rev._ 87, 2007, pp. 1047–1082
  * [2] WHO “The Top 10 Causes of Death” accessed 28 June 2021, Published by World Health Organization (WHO) 2020 Dec 9, 2020
  * [3] CE Rycroft, A. Heyes, L. Lanza and K. Becker “Epidemiology of chronic obstructive pulmonary disease: a literature review” In _Int J Chron Obstruct Pulmon Dis_ 7, 2012, pp. 457–494
  * [4] AJ Guarascio, SM Ray, CK Finch and TH Self “The clinical and economic burden of chronic obstructive pulmonary disease in the USA” In _Clinicoecon Outcomes Res_ 5, 2013, pp. 235–245
  * [5] D Singh, A Agusti, A Anzueto, PJ Barnes, J Bourbeau, BR Celli, GJ Criner, P Frith, DMG Halpin and M Han “Global Strategy for the Diagnosis, Management, and Prevention of Chronic Obstructive Lung Disease: the GOLD science committee report 2019” In _Eur Respir J_ 53, 2019, pp. 1900164
  * [6] Björn W. Schuller, Dagmar M. Schuller, Kun Qian, Juan Liu, Huaiyuan Zheng and Xiao Li “COVID-19 and Computer Audition: An Overview on What Speech & Sound Analysis Could Contribute in the SARS-CoV-2 Corona Crisis” In _CoRR_ abs/2003.11117, 2020
  * [7] Enas Elsayed Mohamed and Riham Ali El maghraby “Voice changes in patients with chronic obstructive pulmonary disease” In _Egyptian Journal of Chest Diseases and Tuberculosis_ 63.3 Elsevier, 2014, pp. 561–567
  * [8] Michael G Crooks, Albertus Den Brinker, Yvette Hayman, James D Williamson, Andrew Innes, Caroline E Wright, Peter Hill and Alyn H Morice “Continuous cough monitoring using ambient sound recording during convalescence from a COPD exacerbation” In _Lung_ 195.3 Springer, 2017, pp. 289–294
  * [9] Viswam Nathan, Korosh Vatanparvar, Md Mahbubur Rahman, Ebrahim Nemati and Jilong Kuang “Assessment of Chronic Pulmonary Disease Patients Using Biomarkers from Natural Speech Recorded by Mobile Devices” In _16th Int. Conf. on Wearable and Implantable Body Sensor Networks (BSN)_ , 2019, pp. 1–4
  * [10] Obaid Ashraf, Erica Rabold, Katrina Schlichtkrull, Anil Singh, Satya Venneti, Mir Mohammed Daanish Ali Khan, Rajat Kulshreshtha and Prakhar Pradeep Naval “Voice-based screening and monitoring of chronic respiratory conditions” In _Chest_ 158.4 Elsevier, 2020, pp. A1687
  * [11] Julia Merkus, Ferdy Hubers, Catia Cucchiarini and Helmer Strik “Digital Eavesdropper – Acoustic Speech Characteristics as Markers of Exacerbations in COPD Patients” In _Proc. RaPID workshop of the 12th LREC_ , 2020, pp. 78
  * [12] David Cleres, Frank Rassouli, Martin Brutsche, Tobias Kowatsch and Filipe Barata “Lena: a Voice-Based Conversational Agent for Remote Patient Monitoring in Chronic Obstructive Pulmonary Disease” In _Proc. ACM Conference on Intelligent User Interfaces_ , 2021
  * [13] Mireia Farrús, Joan Codina-Filbà, Elisenda Reixach, Erik Andrés, Mireia Sans, Noemı́ Garcia and Josep Vilaseca “Speech-Based Support System to Supervise Chronic Obstructive Pulmonary Disease Patient Status” In _Applied Sciences_ 11.17 Multidisciplinary Digital Publishing Institute, 2021, pp. 7999
  * [14] Ognjen Rudovic, Jaeryoung Lee, Miles Dai, Björn Schuller and Rosalind W Picard “Personalized machine learning for robot perception of affect and engagement in autism therapy” In _Science Robotics_ 3.19 AAAS, 2018, pp. 1–11
  * [15] Andreas Triantafyllopoulos, Shuo Liu and Björn W Schuller “Deep speaker conditioning for speech emotion recognition” In _Proc. of the IEEE International Conference on Multimedia and Expo (ICME)_ Shenzhen, China: IEEE, 2021, pp. 1–6
  * [16] F. Schiel “Automatic Phonetic Transcription of Non-Prompted Speech” In _Proc. ICPhS14_ , 1999, pp. 607–610
  * [17] Thomas Kisler, Uwe Reichel and Florian Schiel “Multilingual processing of speech via web services” In _Computer Speech & Language_ 45, Virtual Special Issues Elsevier, 2017, pp. 326–347 DOI: 10.1016/j.csl.2017.01.005
  * [18] Florian Eyben, Klaus R Scherer, Björn W Schuller, Johan Sundberg, Elisabeth André, Carlos Busso, Laurence Y Devillers, Julien Epps, Petri Laukka and Shrikanth S Narayanan “The Geneva minimalistic acoustic parameter set (GeMAPS) for voice research and affective computing” In _IEEE transactions on affective computing_ 7.2 IEEE, 2015, pp. 190–202
  * [19] Katrin D Bartl-Pokorny, Florian B Pokorny, Anton Batliner, Shahin Amiriparian, Anastasia Semertzidou, Florian Eyben, Elena Kramer, Florian Schmidt, Rainer Schönweiler and Markus Wehler “The voice of COVID-19: Acoustic correlates of infection in sustained vowels” In _JASA_ 149.6 Acoustical Society of America, 2021, pp. 4377–4383
  * [20] Florian Eyben, Martin Wöllmer and Björn Schuller “Opensmile: the munich versatile and fast open-source audio feature extractor” In _Proc. 18th ACM international conference on Multimedia_ , 2010, pp. 1459–1462
  * [21] Björn Schuller, Stefan Steidl, Anton Batliner, Alessandro Vinciarelli, Klaus Scherer, Fabien Ringeval, Mohamed Chetouani, Felix Weninger, Florian Eyben and Erik Marchi “The INTERSPEECH 2013 computational paralinguistics challenge: Social signals, conflict, emotion, autism” In _Proc. Interspeech, Lyon, France_ , 2013
  * [22] Alexei Baevski, Yuhao Zhou, Abdelrahman Mohamed and Michael Auli “wav2vec 2.0: A framework for self-supervised learning of speech representations” In _Advances in Neural Information Processing Systems_ 33, 2020, pp. 12449–12460
  * [23] Alexis Conneau, Alexei Baevski, Ronan Collobert, Abdelrahman Mohamed and Michael Auli “Unsupervised Cross-Lingual Representation Learning for Speech Recognition” In _Proc. Interspeech_ , 2021, pp. 2426–2430
  * [24] Scott M Lundberg and Su-In Lee “A unified approach to interpreting model predictions” In _Advances in neural information processing systems_ 30, 2017, pp. 4768–4777
  * [25] Anton Batliner and Bernd Möbius “Prosody in Automatic Speech Processing” In _The Oxford Handbook of Language Prosody_ Oxford, UK: Oxford University Press, 2020, pp. 633–645
  * [26] Florian Hönig, Anton Batliner, Elmar Nöth, Sebastian Schnieder and Jarek Krajewski “Automatic modelling of depressed speech: relevant features and relevance of gender” In _Proc. Interspeech 2014_ , 2014, pp. 1248–1252
  * [27] K. Ishikawa and J. Webster “The Formant Bandwidth as a Measure of Vowel Intelligibility in Dysphonic Speech” Published online: October 31, 2020 In _J Voice_ 20, 2020
  * [28] Alain De Cheveigné “Formant bandwidth affects the identification of competing vowels” In _Proc. ICPhS14_ , 1999, pp. 2093–2096
  * [29] KK Baker, LO Ramig and S Sapir “Control of Vocal Loudness in Young and Old Adults.” In _Journal of Speech, Language & Hearing Research_ 44.2 American Speech-Language-Hearing Association, 2001, pp. 297–304
  * [30] James M Hillenbrand and Robert Houde “Acoustic correlates of breathy vocal quality: Dysphonic voices and continuous speech” In _Journal of Speech and Hearing Research_ 39, 1996, pp. 311–321
  * [31] M. Södersten and P.. Lindestad “Glottal closure and perceived breathiness during phonation in normally speaking subjects” In _J Speech Hear Res._ 33, 1990, pp. 601–611
  * [32] A. Batliner, S. Burger, B. Johne and A. Kießling “MÜSLI: A Classification Scheme For Laryngealizations” In _Proc. ESCA Workshop on Prosody_ , 1993, pp. 176–179
  * [33] Patricia Keating, Marc Garellek and Jody Kreiman “Acoustic properties of different kinds of creaky voice” In _Proc. ICPhS18_ , 2015, pp. 1–5
  * [34] M. Cernak, J.R. Orozco-Arroyave, F. Rudzicz, H. Christensen, J.C. Vásquez-Correa and E. Nöth “Characterisation of voice quality of Parkinson’s disease using differential phonological posterior features” In _Computer Speech & Language_ 46, 2017, pp. 196–208


* Fang and Sighireanu (2017a) Bin Fang and Mihaela Sighireanu. 2017a.  Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators. In _Proceedings of International Symposium on Logic-Based Program Synthesis and Transformation_. Springer International Publishing, 151–167.
  * Fang and Sighireanu (2017b) Bin Fang and Mihaela Sighireanu. 2017b.  A Refinement Hierarchy for Free List Memory Allocators. In _Proceedings of ACM SIGPLAN International Symposium on Memory Management_. ACM, 104–114.
  * Fang et al. (2018) Bin Fang, Mihaela Sighireanu, Geguang Pu, Wen Su, Jean-Raymond Abrial, Mengfei Yang, and Lei Qiao. 2018.  Formal Modelling of List based Dynamic Memory Allocators.  _Science China Information Sciences_ 61, 12 (13 Nov 2018), 103 – 122.
  * Gallardo et al. (2009) María del Mar Gallardo, Pedro Merino, and David Sanán. 2009\.  Model Checking Dynamic Memory Allocation in Operating Systems.  _Journal of Automated Reasoning_ 42, 2 (April 2009), 229–264.
  * Gu et al. (2015) Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015\.  Deep Specifications and Certified Abstraction Layers. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ _(POPL’15)_. ACM, New York, NY, USA, 595–608.
  * Gu et al. (2016) Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016.  CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In _Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)_. USENIX Association, Savannah, GA, 653–669.
  * Gu et al. (2018) Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018\.  Certified Concurrent Abstraction Layers. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation_ _(PLDI 2018)_. ACM, New York, NY, USA, 646–661.
  * Kirchner et al. (2015) Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015\.  Frama-C: A Software Analysis Perspective.  _Formal Aspects of Computing_ 27, 3 (01 May 2015), 573–609.
  * Klein (2009) Gerwin Klein. 2009\.  Operating System Verification - An Overview.  _Sadhana_ 34, 1 (February 2009), 27–69.
  * Klein et al. (2014) Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014.  Comprehensive Formal Verification of an OS Microkernel.  _ACM Transactions on Computer Systems_ 32, 1 (2014), 2:1–2:70.
  * Klein et al. (2009) Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. 2009\.  seL4: Formal Verification of an OS Kernel. In _Proceedings of 22nd ACM SIGOPS Symposium on Operating Systems Principles (SOSP)_. ACM Press, 207–220.
  * Klein and Tuch (2004) Gerwin Klein and Harvey Tuch. 2004.  Towards Verified Virtual Memory in L4. In _Proceedings of TPHOLs Emerging Trends_. Park City, Utah, USA, 16 pages.
  * Knowlton (1965) Kenneth C. Knowlton. 1965\.  A Fast Storage Allocator.  _Communication of the ACM_ 8, 10 (1965), 623–624.
  * Kroening and Tautschnig (2014) Daniel Kroening and Michael Tautschnig. 2014.  CBMC – C Bounded Model Checker. In _Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_ , Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 389–391.
  * Leinenbach, Dirk and Santen, Thomas (2009) Leinenbach, Dirk and Santen, Thomas. 2009\.  Verifying the Microsoft Hyper-V Hypervisor with VCC. In _Proceedings of International Symposium on Formal Methods_. Springer Berlin Heidelberg, Berlin, Heidelberg, 806–809.
  * Leroy and Blazy (2008) Xavier Leroy and Sandrine Blazy. 2008.  Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations.  _Journal of Automated Reasoning_ 41, 1 (01 July 2008), 1–31.
  * Mansky et al. (2015) William Mansky, Dmitri Garbuzov, and Steve Zdancewic. 2015\.  An Axiomatic Specification for Sequential Memory Models. In _Proceedings of International Conference on Computer Aided Verification (CAV)_. Springer International Publishing, 413–428.
  * Mantel et al. (2011) Heiko Mantel, David Sands, and Henning Sudbrock. 2011\.  Assumptions and Guarantees for Compositional Noninterference. In _Proceedings of 24th Computer Security Foundations Symposium (CSF)_. IEEE Press, 218–232.
  * Marti et al. (2006) Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. 2006\.  Formal Verification of the Heap Manager of an Operating System Using Separation Logic. In _Proceedings of International Conference on Formal Engineering Methods (ICFEM)_. Springer Berlin Heidelberg, Berlin, Heidelberg, 400–419.
  * Murray et al. (2013) TS Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Carmen Lewis, Xin Gao, and Gary Klein. 2013.  seL4: From General Purpose to a Proof of Information Flow Enforcement. In _Proceedings of 2013 IEEE Symposium on Security and Privacy (S &P)_. IEEE Press, 415–429.
  * Murray et al. (2012) Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, and Gerwin Klein. 2012.  Noninterference for Operating System Kernels. In _Proceedings of 2nd International Conference on Certified Programs and Proofs (CPP)_. Springer, 126–142.
  * Murray et al. (2018) T. Murray, R. Sison, and K. Engelhardt. 2018.  COVERN: A Logic for Compositional Verification of Information Flow Control. In _Proceedings of 2018 IEEE European Symposium on Security and Privacy (EuroS &P)_. 16–30.
  * Murray et al. (2016) Toby Murray, Robert Sison, Edward Pierzchalski, and Christine Rizkallah. 2016.  Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In _Proceedings of 29th IEEE Computer Security Foundations Symposium (CSF)_. IEEE Press.
  * Nelson et al. (2017) Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017.  Hyperkernel: Push-Button Verification of an OS Kernel. In _Proceedings of the 26th Symposium on Operating Systems Principles_ _(SOSP ’17)_. ACM, New York, NY, USA, 252–269.
  * Rushby (1992) John Rushby. 1992\.  _Noninterference, Transitivity, and Channel-control Security Policies_.  Technical Report. SRI International, Computer Science Laboratory.
  * Sabelfeld and Myers (2003) Andrei Sabelfeld and Andrew C Myers. 2003.  Language-based Information-Flow Security.  _IEEE Journal on Selected Areas in Communications_ 21, 1 (January 2003), 5–19.
  * Sanán et al. (2017) David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, and Yang Liu. 2017.  CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. In _Proceedings of 23rd International ConferenceTools and Algorithms for the Construction and Analysis of Systems (TACAS)_. 481–498.
  * Sanan et al. (2021) David Sanan, Yongwang Zhao, Shangwei Lin, and Liu Yang. 2021\.  CSim2: Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee.  _ACM Transactions on Programming Languages and Systems_ 43, 1, Article 2 (February 2021), 46 pages.
  * Saraswat et al. (2007) Vijay A. Saraswat, Radha Jagadeesan, Maged Michael, and Christoph von Praun. 2007.  A Theory of Memory Models. In _Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)_. ACM, 161–172.
  * Schirmer (2006) N. Schirmer. 2006\.  _Verification of Sequential Imperative Programs in Isabelle/HOL_.  Ph.D. Dissertation. Technischen Universitat Munchen.
  * Su et al. (2016) Wen Su, Jean Raymond Abrial, Geguang Pu, and Bin Fang. 2016\.  Formal Development of a Real-Time Operating System Memory Manager. In _Proceedings of International Conference on Engineering of Complex Computer Systems (ICECCS)_. 130–139.
  * Tews et al. (2009) Hendrik Tews, Marcus Völp, and Tjark Weber. 2009\.  Formal Memory Models for the Verification of Low-Level Operating-System Code.  _Journal of Automated Reasoning_ 42, 2 (01 April 2009), 189–227.
  * Vaynberg and Shao (2012) Alexander Vaynberg and Zhong Shao. 2012.  Compositional Verification of a Baby Virtual Memory Manager. In _Proceedings of 2nd International Conference on Certified Programs and Proofs (CPP)_. Springer-Verlag, Berlin, Heidelberg, 143–159.
  * von Oheimb (2004) David von Oheimb. 2004\.  Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage. In _Proceedings of 9th European Symposium on Research in Computer Security (ESORICS)_. Springer, 225–243.
  * Ševčík et al. (2013) Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2013.  CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.  _J. ACM_ 60, 3, Article 22 (June 2013), 50 pages.
  * Xu et al. (2016) Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. 2016\.  A Practical Verification Framework for Preemptive OS Kernels. In _Proceedings of 28th International Conference on Computer Aided Verification (CAV)_. Springer, 59–79.
  * Yang and Hawblitzel (2011) Jean Yang and Chris Hawblitzel. 2011.  Safe to the Last Instruction: Automated Verification of a Type-safe Operating System.  _Communnication of the ACM_ 54, 12 (2011), 123–131.
  * Yu et al. (2003) Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. 2003.  Building Certified Libraries for PCC: Dynamic Storage Allocation. In _Proceedings of European Symposium on Programming Languages and Systems (ESOP)_. Springer Berlin Heidelberg, 363–379.
  * Zhao and Sanán (2019) Yongwang Zhao and David Sanán. 2019.  Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS. In _Proceedings of 31st International Conference on Computer Aided Verification (CAV)_. Springer International Publishing, 515–533.
  * Zhao et al. (2019a) Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. 2019a.  A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. In _Proceedings of 23rd International Symposium on Formal Methods (FM)_. Springer International Publishing, 161–178.
  * Zhao et al. (2019b) Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. 2019b.  Refinement-Based Specification and Security Analysis of Separation Kernels.  _IEEE Transactions on Dependable and Secure Computing_ 16, 1 (Jan 2019), 127–141.
  * Zhao et al. (2017) Yongwang Zhao, Zhibin Yang, and Dianfu Ma. 2017.  A Survey on Formal Specification and Verification of Separation Kernels.  _Frontiers of Computer Science_ 11, 4 (2017), 585 – 607.

##  Appendix A C Code of _k_mem_pool_free_

⬇

1static void free_block(struct k_mem_pool *p, int level, size_t *lsizes, int
bn)

2{

3 int i, key, lsz = lsizes[level];

4 void *block = block_ptr(p, lsz, bn);

5

6 key = irq_lock();

7

8 set_free_bit(p, level, bn);

9

10 if (level && partner_bits(p, level, bn) == 0xf) {

11 for (i = 0; i < 4; i++) {

12 int b = (bn & ~3) + i;

13

14 clear_free_bit(p, level, b);

15 if (b != bn && block_fits(p, block_ptr(p, lsz, b), lsz)) {

16 sys_dlist_remove(block_ptr(p, lsz, b));

17 }

18 }

19

20 irq_unlock(key);

21 free_block(p, level-1, lsizes, bn / 4); /* tail recursion! */

22 return;

23 }

24

25 if (block_fits(p, block, lsz)) {

26 sys_dlist_append(&p->levels[level].free_list, block);

27 }

28

29 irq_unlock(key);

30}

31

32void k_mem_pool_free(struct k_mem_block *block)

33{

34 int i, key, need_sched = 0;

35 struct k_mem_pool *p = get_pool(block->id.pool);

36 size_t lsizes[p->n_levels];

37

38 /* As in k_mem_pool_alloc(), we build a table of level sizes

39 * to avoid having to store it in precious RAM bytes.

40 * Overhead here is somewhat higher because free_block()

41 * doesn’t inherently need to traverse all the larger

42 * sublevels.

43 */

44 lsizes[0] = _ALIGN4(p->max_sz);

45 for (i = 1; i <= block->id.level; i++) {

46 lsizes[i] = _ALIGN4(lsizes[i-1] / 4);

47 }

48

49 free_block(get_pool(block->id.pool), block->id.level, lsizes,
block->id.block);

50

51 /* Wake up anyone blocked on this pool and let them repeat

52 * their allocation attempts

53 */

54 key = irq_lock();

55

56 while (!sys_dlist_is_empty(&p->wait_q)) {

57 struct k_thread *th = (void *)sys_dlist_peek_head(&p->wait_q);

58

59 _unpend_thread(th);

60 _abort_thread_timeout(th);

61 _ready_thread(th);

62 need_sched = 1;

63 }

64

65 if (need_sched && !_is_in_isr()) {

66 _reschedule_threads(key);

67 } else {

68 irq_unlock(key);

69 }

70}

##  Appendix B Specification and Proof Sketch of _k_mem_pool_free_

The formal specification of _k_mem_pool_free_ (in _black_ color) and its rely-
guarantee proof sketch (in _blue_ color) are shown as follows.

_Mem -pool-free-pre_ t  _$\equiv$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_ _´_ inv
_$\wedge$_  _´_ allocating-node t  _$=$_ None  _$\wedge$_  _´_ freeing-node t
_$=$_ None _$\mathclose{\mid\mkern-4.5mu\\}}$_

_EVENT_  _Mem -pool-free_ [Block b] @  _$($_ $\mathcal{T}$ t _$)$_

_WHEN_

pool b  _$\in$_  _´_ mem-pools

 _$\wedge$_ level b  _$ <$_ length  _$($_ levels  _$($__´_ mem-pool-info
_$($_ pool b _$)$__$)$__$)$_

 _$\wedge$_ block b  _$ <$_ length  _$($_ bits  _$($_ levels  _$($__´_ mem-
pool-info  _$($_ pool b _$)$__$)$__$!$__$($_ level b _$)$__$)$__$)$_

 _$\wedge$_ data b  _$=$_ block-ptr  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_

 _$($__$($_ ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$)$_ div  _$($_ 4 ^  _$($_ level b _$)$__$)$__$)$_  _$($_
block b _$)$_

_THEN_

Mem-pool-free-pre t  _$\cap$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_ g
_$\mathclose{\mid\mkern-4.5mu\\}}$_ (* g is the guard condition of the event
*)

_$($__$*$_ here we set the bit to FREEING _$\mathord{,}$_ so that other thread
cannot mem-pool-free the same block

it also requires that it can only free ALLOCATED block  _$*$__$)$_

t $\blacktriangleright$  _AWAIT_  _$($_ bits  _$($__$($_ levels  _$($__´_ mem-
pool-info  _$($_ pool b _$)$__$)$__$)$_  _$!$_  _$($_ level b _$)$__$)$__$)$_
_$!$_  _$($_ block b

_$=$_ ALLOCATED  _THEN_

_´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-freeing  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($_ level b _$)$_  _$($_ block b
_$)$__$\mathord{;}$__$\mathord{;}$_

_´_ freeing-node  _$\mathord{:}$__$=$_  _´_ freeing-node  _$($_ t
_$\mathord{:}$__$=$_ Some b _$)$_

_END_ _$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-precond1_ t b  _$\equiv$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_ _´_
inv  _$\wedge$_  _´_ allocating-node t  _$=$_ None  _$\wedge$_ g  _$\wedge$_
_´_ freeing-node t  _$=$_ Some b _$\mathclose{\mid\mkern-4.5mu\\}}$_

(* remove the mem block from the thread’s allocated block set *)

t $\blacktriangleright$  _´_ mblocks := _´_ mblocks(t:=_´_ mblocks t -
{_$\mathopen{\\{\mkern-4.5mu\mid}$_ pool = (pool b), level=_´_ lvl t,block=_´_
bn t,

data=block_ptr (_´_ mem_pool_info (pool b))

(((ALIGN4 (max_sz (_´_ mem_pool_info (pool b)))) div (4 ^ (_´_ lvl t)))) (_´_
bn t) _$\mathclose{\mid\mkern-4.5mu\\}}$_});;

_mp -free-precond2_ t b  _$\equiv$_  _mp -free-precond1_ t b

t $\blacktriangleright$  _´_ need-resched  _$\mathord{:}$__$=$_  _´_ need-
resched _$($_ t  _$\mathord{:}$__$=$_ False
_$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-precond3_ t b  _$\equiv$_  _$($_ mp-free-precond2 t b _$)$_
_$\cap$_  _$\mathopen{\\{\mkern-4.5mu\mid}$__´_ need-resched t  _$=$_ False
_$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _´_ lsizes  _$\mathord{:}$__$=$_  _´_ lsizes _$($_ t
_$\mathord{:}$__$=$_  _$[$_ ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info
_$($_ pool b _$)$__$)$__$)$__$]$__$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-precond4_ t b  _$\equiv$_

mp-free-precond3 t b  _$\cap$_  _$\mathopen{\\{\mkern-4.5mu\mid}$__´_ lsizes t
_$=$_  _$[$_ ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$]$__$\mathclose{\mid\mkern-4.5mu\\}}$_

_FOR_  _$($_ t $\blacktriangleright$  _´_ i  _$\mathord{:}$__$=$_  _´_ i _$($_
t  _$\mathord{:}$__$=$_ 1 _$)$__$)$__$\mathord{;}$_ _´_ i t  _$\leq$_ level b
_$\mathord{;}$_  _$($_ t $\blacktriangleright$  _´_ i  _$\mathord{:}$__$=$_
_´_ i _$($_ t  _$\mathord{:}$__$=$_  _´_ i t  _$+$_ 1 _$)$__$)$_  _DO_

t $\blacktriangleright$  _´_ lsizes  _$\mathord{:}$__$=$_  _´_ lsizes _$($_ t
_$\mathord{:}$__$=$_  _´_ lsizes t  _$@$_  _$[$_ ALIGN4  _$($__´_ lsizes t
_$!$_  _$($__´_ i t  _$-$_ 1 _$)$_ div 4 _$)$__$]$__$)$_

_ROF_ _$\mathord{;}$__$\mathord{;}$_

_mp -free-precond5_ t b  _$\equiv$_ mp-free-precond3 t b  _$\cap$_

 _$\mathopen{\\{\mkern-4.5mu\mid}$__$($__$\forall\,$_ ii _$ <$_length
_$($__´_ lsizes t _$)$__$\mathord{.}$_  _´_ lsizes t  _$!$_ ii  _$=$_  _$($_
ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$)$_

div  _$($_ 4 ^ ii _$)$__$)$_  _$\wedge$_ length  _$($__´_ lsizes t _$)$_  _$
>$_ level b _$\mathclose{\mid\mkern-4.5mu\\}}$_

_$($__$*$_  _$=$_ _$=$_ _$=$_ start _$\mathord{:}$_ free-block _$($_ pool
_$\mathord{,}$_ level _$\mathord{,}$_ lsizes _$\mathord{,}$_ block
_$)$__$\mathord{;}$_  _$=$_ _$=$_ _$=$__$*$__$)$_

t $\blacktriangleright$  _´_ free-block-r  _$\mathord{:}$__$=$_  _´_ free-
block-r  _$($_ t  _$\mathord{:}$__$=$_ True
_$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-precond6_ t b  _$\equiv$_ mp-free-precond5 t b  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$__´_ free-block-r t  _$=$_ True
_$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _´_ bn  _$\mathord{:}$__$=$_  _´_ bn  _$($_ t
_$\mathord{:}$__$=$_ block b _$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-precond7_ t b  _$\equiv$_ mp-free-precond6 t b  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$__´_ bn t  _$=$_ block b
_$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _´_ lvl  _$\mathord{:}$__$=$_  _´_ lvl  _$($_ t
_$\mathord{:}$__$=$_ level b _$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-loopinv_ t b  _$\alpha$_

 _WHILE_  _´_ free-block-r t  _DO_

_mp -free-cnd1_ t b  _$\alpha$_  _$\equiv$_ mp-free-loopinv t b  _$\alpha$_
_$\cap$_ _$\mathopen{\\{\mkern-4.5mu\mid}$_ _$\alpha$_ _$ >$_ 0
_$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _´_ lsz  _$\mathord{:}$__$=$_  _´_ lsz  _$($_ t
_$\mathord{:}$__$=$_  _´_ lsizes t  _$!$_  _$($__´_ lvl t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-cnd2_ t b  _$\alpha$_  _$\equiv$_ mp-free-cnd1 t b  _$\alpha$_
_$\cap$_ _$\mathopen{\\{\mkern-4.5mu\mid}$_ _´_ lsz t  _$=$_  _´_ lsizes t
_$!$_  _$($__´_ lvl t _$)$_ _$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _´_ blk  _$\mathord{:}$__$=$_  _´_ blk  _$($_ t
_$\mathord{:}$__$=$_ block-ptr  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_  _$($__´_ lsz t _$)$_  _$($__´_ bn t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

_mp -free-cnd3_ t b  _$\alpha$_  _$\equiv$_ mp-free-cnd2 t b  _$\alpha$_
_$\cap$_

 _$\mathopen{\\{\mkern-4.5mu\mid}$_ _´_ blk t  _$=$_ block-ptr  _$($__´_ mem-
pool-info  _$($_ pool b _$)$__$)$_  _$($__´_ lsz t _$)$_  _$($__´_ bn t _$)$_
_$\mathclose{\mid\mkern-4.5mu\\}}$_

t $\blacktriangleright$  _ATOM_

{V1} _$($_ V1 _$\in$_ mp-free-cnd3 t b  _$\alpha$_ _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$__´_ cur  _$=$_ Some t
_$\mathclose{\mid\mkern-4.5mu\\}}$__$)$_

 _´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-free  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t
_$)$__$\mathord{;}$__$\mathord{;}$_

{V2} _$($_ V2 = V1 _$\mathopen{(\mkern-3.0mu\mid}$_ mem-pool-info
_$\mathord{:}$__$=$_

set-bit-free  _$($_ mem-pool-info V1 _$)$_  _$($_ pool b _$)$_  _$($_ lvl V1 t
_$)$_  _$($_ bn V1 t _$)$__$\mathclose{\mid\mkern-3.0mu)}$__$)$_

 _´_ freeing-node  _$\mathord{:}$__$=$_  _´_ freeing-node  _$($_ t
_$\mathord{:}$__$=$_ None _$)$__$\mathord{;}$__$\mathord{;}$_

{V3} _$($_ V3 = V2 _$\mathopen{(\mkern-3.0mu\mid}$_ freeing-node
_$\mathord{:}$__$=$_  _$($_ freeing-node V2 _$)$__$($_ t  _$\mathord{:}$__$=$_
None _$)$__$\mathclose{\mid\mkern-3.0mu)}$__$)$_

 _IF_  _´_ lvl t  _$ >$_ 0  _$\wedge$_ partner-bits  _$($__´_ mem-pool-info
_$($_ pool b _$)$__$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t _$)$_  _THEN_

(V3 _$\in$_ _$\mathopen{\\{\mkern-4.5mu\mid}$_ NULL  _$ <$_  _´_ lvl t
_$\wedge$_ partner-bits  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_
_$($__´_ lvl t _$)$_  _$($__´_ bn t _$)$__$\mathclose{\mid\mkern-4.5mu\\}}$_)

_mergeblock -loopinv_ V3 t b  _$\alpha$_  _$\equiv$_

 _$\\{$_ V _$\mathord{.}$_ let minf0  _$=$_  _$($_ mem-pool-info V3 _$)$__$($_
pool b _$)$__$\mathord{;}$_ lvl0  _$=$_  _$($_ levels minf0 _$)$_  _$!$_
_$($_ lvl V3 t _$)$__$\mathord{;}$_

minf1  _$=$_  _$($_ mem-pool-info V _$)$__$($_ pool b _$)$__$\mathord{;}$_
lvl1  _$=$_  _$($_ levels minf1 _$)$_  _$!$_  _$($_ lvl V3 t _$)$_ in

 _$($_ bits lvl1  _$=$_ list-updates-n  _$($_ bits lvl0 _$)$_  _$($__$($_ bn
V3 t div 4 _$)$_  _$*$_ 4 _$)$_  _$($_ i V t _$)$_ NOEXIST _$)$_

 _$\wedge$_  _$($_ free-list lvl1  _$=$_ removes  _$($_ map  _$($__$\lambda$_
ii _$\mathord{.}$_ block-ptr minf0  _$($_ lsz V3 t _$)$_

 _$($__$($_ bn V3 t div 4 _$)$_  _$*$_ 4  _$+$_ ii _$)$__$)$_  _$[$_ 0
_$\mathord{.}$__$\mathord{.}$__$ <$__$($_ i V t _$)$__$]$__$)$_  _$($_ free-
list lvl0 _$)$__$)$_

_$\wedge$_  _$($_ wait-q minf0  _$=$_ wait-q minf1 _$)$_  _$\wedge$_
_$($__$\forall\,$_ t _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{.}$_
t _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_  _$\not=$_ t  _$\longrightarrow$_
lvars-nochange t _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ V V3 _$)$_

_$\wedge$_  _$($__$\forall\,$_ p _$\mathord{.}$_ p  _$\not=$_ pool b
_$\longrightarrow$_ mem-pool-info V p  _$=$_ mem-pool-info V3 p _$)$_

 _$\wedge$_  _$($__$\forall\,$_ j _$\mathord{.}$_ j  _$\not=$_ lvl V3 t
_$\longrightarrow$_  _$($_ levels minf0 _$)$__$!$_ j  _$=$_  _$($_ levels
minf1 _$)$__$!$_ j _$)$_

_$\wedge$_  _$($_ V _$\mathord{,}$_ V3 _$)$__$\in$_ gvars-conf-stable
_$\wedge$_ i V t  _$\leq$_ 4  _$\wedge$_  _$\wedge$_  _$\alpha$_ = 4 - i V t
…… _$\\}$_

_FOR_  _´_ i  _$\mathord{:}$__$=$_  _´_ i _$($_ t  _$\mathord{:}$__$=$_ 0
_$)$__$\mathord{;}$_  _´_ i t  _$ <$_ 4 _$\mathord{;}$_  _´_ i
_$\mathord{:}$__$=$_  _´_ i _$($_ t  _$\mathord{:}$__$=$_  _´_ i t  _$+$_ 1
_$)$_  _DO_

_mergeblock -loopinv_ V3 t b  _$\alpha$_  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$_ _$\alpha$_ _$ >$_ 0
_$\mathclose{\mid\mkern-4.5mu\\}}$_

{V4} _$($_ V4 _$\in$_ mergeblock-loopinv V3 t b  _$\alpha$_  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$_ _$\alpha$_ _$ >$_ 0
_$\mathclose{\mid\mkern-4.5mu\\}}$_ _$)$_

_´_ bb  _$\mathord{:}$__$=$_  _´_ bb  _$($_ t  _$\mathord{:}$__$=$_  _$($__´_
bn t div 4 _$)$_  _$*$_ 4  _$+$_  _´_ i t _$)$__$\mathord{;}$__$\mathord{;}$_

{V5} _$($_ V5 _$\equiv$_ V4 _$\mathopen{(\mkern-3.0mu\mid}$_ bb
_$\mathord{:}$__$=$_  _$($_ bb V _$)$_  _$($_ t _$\mathord{:}$__$=$__$($_ bn
V4 t div 4 _$)$_  _$*$_ 4  _$+$_ i V4 t _$)$__$\mathclose{\mid\mkern-3.0mu)}$_
_$)$_

_´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-noexist  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bb t
_$)$__$\mathord{;}$__$\mathord{;}$_

{V6} _$($_ V6 _$\equiv$_ V5 _$\mathopen{(\mkern-3.0mu\mid}$_ mem-pool-info
_$\mathord{:}$__$=$_

set-bit-noexist (mem-pool-info V5) (pool b) (lvl V5 t) (bb V5 t)
_$\mathclose{\mid\mkern-3.0mu)}$_ _$)$_

_´_ block-pt  _$\mathord{:}$__$=$_  _´_ block-pt  _$($_ t
_$\mathord{:}$__$=$_ block-ptr  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_  _$($__´_ lsz t _$)$_  _$($__´_ bb t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

{V7} _$($_ V7 _$\equiv$_ V6 _$\mathopen{(\mkern-3.0mu\mid}$_ block-pt
_$\mathord{:}$__$=$_  _$($_ block-pt V6 _$)$_

 _$($_ t _$\mathord{:}$__$=$_ block-ptr  _$($_ mem-pool-info V6  _$($_ pool b
_$)$__$)$_  _$($_ lsz V6 t _$)$_  _$($_ bb V6 t
_$)$__$)$__$\mathclose{\mid\mkern-3.0mu)}$_ _$)$_

_IF_  _´_ bn t  _$\not=$_  _´_ bb t  _$\wedge$_ block-fits  _$($__´_ mem-pool-
info  _$($_ pool b _$)$__$)$_  _$($__´_ block-pt t _$)$_  _$($__´_ lsz t _$)$_
_THEN_

 _´_ mem-pool-info  _$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($__$($_ pool b
_$)$_  _$\mathord{:}$__$=$_

remove-free-list  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_
lvl t _$)$_  _$($__´_ block-pt t _$)$__$)$_

 _FI_

 _ROF_ _$\mathord{;}$__$\mathord{;}$_

_mergeblock -loopinv_ V3 t b  _$\alpha$_  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$_ _$\alpha$_ = 0
_$\mathclose{\mid\mkern-4.5mu\\}}$_

_´_ lvl  _$\mathord{:}$__$=$_  _´_ lvl  _$($_ t  _$\mathord{:}$__$=$_  _´_ lvl
t  _$-$_ 1 _$)$__$\mathord{;}$__$\mathord{;}$_

 _´_ bn  _$\mathord{:}$__$=$_  _´_ bn  _$($_ t  _$\mathord{:}$__$=$_  _´_ bn t
div 4 _$)$__$\mathord{;}$__$\mathord{;}$_

 _´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-freeing  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t
_$)$__$\mathord{;}$__$\mathord{;}$_

 _´_ freeing-node  _$\mathord{:}$__$=$_  _´_ freeing-node  _$($_ t
_$\mathord{:}$__$=$_ Some  _$\mathopen{(\mkern-3.0mu\mid}$_ pool  _$=$_  _$($_
pool b _$)$__$\mathord{,}$_ level  _$=$_  _$($__´_ lvl t _$)$__$\mathord{,}$_

block  _$=$_  _$($__´_ bn t _$)$__$\mathord{,}$_ data  _$=$_ block-ptr
_$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_

_$($__$($__$($_ ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$)$_ div  _$($_ 4 ^  _$($__´_ lvl t _$)$__$)$__$)$__$)$_
_$($__´_ bn t _$)$_  _$\mathclose{\mid\mkern-3.0mu)}$__$)$_

 _ELSE_

{V3}  _$\cap$_  _$-$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_ NULL  _$ <$_  _´_
lvl t  _$\wedge$_ partner-bits  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t
_$)$__$\mathclose{\mid\mkern-4.5mu\\}}$_

_IF_ block-fits  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_ blk
t _$)$_  _$($__´_ lsz t _$)$_  _THEN_

 _´_ mem-pool-info  _$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($__$($_ pool b
_$)$_  _$\mathord{:}$__$=$_

append-free-list  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_
lvl t _$)$_  _$($__´_ blk t _$)$_  _$)$_

 _FI_ _$\mathord{;}$__$\mathord{;}$_

 _´_ free-block-r  _$\mathord{:}$__$=$_  _´_ free-block-r  _$($_ t
_$\mathord{:}$__$=$_ False _$)$_

 _FI_

 _END_ (* END of ATOM *)

 _OD_ (* END of WHILE free_block_r DO *)

_mp -free-precond9_ t b  _$\equiv$_ Mem-pool-free-pre t  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$_ g _$\mathclose{\mid\mkern-4.5mu\\}}$_

_$($__$*$_  _$=$_ _$=$_ _$=$_ end of _$\mathord{:}$_ free-block _$($_ pool
_$\mathord{,}$_ level _$\mathord{,}$_ lsizes _$\mathord{,}$_ block
_$)$__$\mathord{;}$_  _$=$_ _$=$_ _$=$__$*$__$)$_

t $\blacktriangleright$  _ATOMIC_

{Va} _$($_ Va _$\in$_ mp-free-precond9 t b  _$\cap$_
_$\mathopen{\\{\mkern-4.5mu\mid}$__´_ cur  _$=$_ Some t
_$\mathclose{\mid\mkern-4.5mu\\}}$__$)$_

stm9-loopinv Va t b  _$\alpha$_  _$\equiv$_

 _$\\{$_ V _$\mathord{.}$_ inv V  _$\wedge$_ cur V  _$=$_ cur Va  _$\wedge$_
tick V  _$=$_ tick Va  _$\wedge$_  _$($_ V _$\mathord{,}$_ Va _$)$__$\in$_
gvars-conf-stable

 _$\wedge$_ freeing-node V t  _$=$_ freeing-node Va t  _$\wedge$_ allocating-
node V t  _$=$_ allocating-node Va t

 _$\wedge$_  _$($__$\forall\,$_ p _$\mathord{.}$_ levels  _$($_ mem-pool-info
V p _$)$_  _$=$_ levels  _$($_ mem-pool-info Va p _$)$__$)$_

 _$\wedge$_  _$($__$\forall\,$_ p _$\mathord{.}$_ p  _$\not=$_ pool b
_$\longrightarrow$_ mem-pool-info V p  _$=$_ mem-pool-info Va p _$)$_

 _$\wedge$_  _$($__$\forall\,$_ t _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{.}$_ t _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_  _$\not=$_ t  _$\longrightarrow$_ lvars-
nochange t _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ V Va _$)$_

 _$\wedge$_ _$\alpha$_  _$=$_ length  _$($_ wait-q  _$($__´_ mem-pool-info
_$($_ pool b _$)$__$)$__$)$_ _$\\}$_

_WHILE_ wait-q  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$\not=$_
_$[$__$]$_  _DO_

stm9-loopinv Va t b  _$\alpha$_  _$\cap$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_
_$\alpha$_ _$ >$_ 0 _$\mathclose{\mid\mkern-4.5mu\\}}$_

_´_ th  _$\mathord{:}$__$=$_  _´_ th  _$($_ t  _$\mathord{:}$__$=$_ hd  _$($_
wait-q  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$)$__$\mathord{;}$__$\mathord{;}$_

_$($__$*$_ -unpend-thread _$($_ th _$)$__$\mathord{;}$_  _$*$__$)$_

_´_ mem-pool-info  _$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($_ pool b
_$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($_ pool b _$)$_

_$\mathopen{(\mkern-3.0mu\mid}$_ wait-q  _$\mathord{:}$__$=$_ tl  _$($_ wait-q
_$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$\mathclose{\mid\mkern-3.0mu)}$__$)$__$\mathord{;}$__$\mathord{;}$_

_$($__$*$_ -ready-thread _$($_ th _$)$__$\mathord{;}$_  _$*$__$)$_

_´_ thd-state  _$\mathord{:}$__$=$_  _´_ thd-state  _$($__´_ th t
_$\mathord{:}$__$=$_ READY _$)$__$\mathord{;}$__$\mathord{;}$_

_´_ need-resched  _$\mathord{:}$__$=$_  _´_ need-resched _$($_ t
_$\mathord{:}$__$=$_ True _$)$_

_OD_ _$\mathord{;}$__$\mathord{;}$_

stm9-loopinv Va t b  _$\alpha$_  _$\cap$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_
_$\alpha$_ = 0 _$\mathclose{\mid\mkern-4.5mu\\}}$_

_IF_  _´_ need-resched t  _THEN_

reschedule (* _reschedule_threads(key) *)

 _FI_

 _END_ (* END of ATOM *)

_END_

_Mem -pool-free-post_ t  _$\equiv$_  _$\mathopen{\\{\mkern-4.5mu\mid}$_ _´_
inv  _$\wedge$_  _´_ allocating-node t  _$=$_ None  _$\wedge$_  _´_ freeing-
node t  _$=$_ None _$\mathclose{\mid\mkern-4.5mu\\}}$_