# Striking a Balance between Classical and Deep Learning Approaches in Natural
Language Processing Pedagogy

Aditya Joshi1, Jake Renzella1, Pushpak Bhattacharyya2, Saurav Jha1, Xiangyu
Zhang1
1 University of New South Wales, Sydney, Australia
2 Indian Institute of Technology Bombay, Mumbai, India
<EMAIL_ADDRESS>
<EMAIL_ADDRESS>

###### Abstract

While deep learning approaches represent the state-of-the-art of natural
language processing (NLP) today, classical algorithms and approaches still
find a place in NLP textbooks and courses of recent years. This paper
discusses the perspectives of conveners of two introductory NLP courses taught
in Australia and India, and examines how classical and deep learning
approaches can be balanced within the lecture plan and assessments of the
courses. We also draw parallels with the objects-first and objects-later
debate in CS1 education. We observe that teaching classical approaches adds
value to student learning by building an intuitive understanding of NLP
problems, potential solutions, and even deep learning models themselves.
Despite classical approaches not being state-of-the-art, the paper makes a
case for their inclusion in NLP courses today.

##  1 Introduction

Transformer-based models are the state-of-the-art in natural language
processing (NLP). They represent a new era of deep learning approaches111The
phrase ‘deep learning approaches’ is expected to refer to the broad spectrum
including but not limited to dense word representations, Transformer and
Transformer-based models used in NLP. for NLP. From early work in word
representations to recent approaches in instruction tuning, deep learning
approaches have significantly transformed NLP and many other areas of
artificial intelligence. Universities around the world have incorporated deep
learning approaches in their introductory NLP courses, arguably with varying
speed, and to different extents, as evidenced to an extent, in Table 2). This
puts under question the relevance of classical approaches, i.e., those pre-
dating deep learning approaches, in NLP curricula. This reflection from
academics/faculty members may also be based on questions from students taking
the course who wonder why they should learn about classical approaches, as
seen in pre-course feedback received by the authors of this paper.

Therefore, we analyse the role of classical approaches in the context of
modern university-based courses in NLP. We focus on introductory NLP courses
offered to students of computer science & engineering or equivalent degrees,
and investigate the question:

“How can an introductory NLP course balance between the content covering
classical and deep learning approaches?"

We address the question in two parts: (a) how others do it, and (b) how we do
it. With respect to (a), we describe summaries of NLP textbooks and publicly
available courses in the context of the question. As for (b), we draw insights
from our experience teaching NLP courses at two large, research-intensive
universities in Australia and India. We introduce and discuss our motivations,
considerations and decisions in the lectures, tutorials and projects of NLP
courses. Authors of this paper represent two personas of NLP educators: (a) an
early-career educator who introduced a new NLP course in the beginning of
2024; and (b) a seasoned educator with two-decade experience of teaching and
research experience. The novelty of this paper is as follows:

  1. 1.

There have been papers in the past on specific aspects (tutorials, lecture
content, etc.) of individual NLP courses Plank (2021); Foster and Wagner
(2021); Gaddy et al. (2021). This paper is novel in its comparison of two NLP
courses taught by educators with significantly different experience in NLP
research and pedagogy.

  2. 2.

We also draw parallels to the age-long objects-first or -later debate in
computer science education, to highlight that the classical approaches in NLP
courses can benefit from lessons in computer science education.

  3. 3.

We hope that the paper serves as a useful resource for NLP educators to
examine the role of classical methods in their curricula now and in the
future.

The rest of the paper is described as follows. We first introduce the context
in terms of the two courses being compared in Section 2. Following that, we
discuss an analogous objects first- and objects-later- debate in computer
science education in Section 3. We describe how NLP textbooks and NLP courses
(as per publicly available course outlines) cover classical approaches in
Section 4. We then proceed to compare the lecture plan, and coding assessments
involved in the two courses in Sections 5 and 6 respectively. Section 7 puts
it all together to make our case for the relevance of classical approaches in
NLP courses. Finally, Section 8 concludes the paper.

##  2 Context

The two NLP courses we compare are run at two large universities in Australia
and India, both titled ‘Natural Language Processing’. We refer to these as
NLP-UNSW and NLP-IITB222UNSW: University of New South Wales, Sydney,
Australia; IITB: Indian Institute of Technology Bombay, Mumbai, India.. NLP-
UNSW is the first offering of the course with 60 enrolled students, while NLP-
IITB is the ninteenth offering of the course with 150 enrolled students. While
NLP-UNSW is the only NLP-focussed course at UNSW at the time of writing this
paper, NLP-IITB is accompanied with a ‘Deep learning for NLP’ course which
often follows NLP-IITB. Both courses were offered as an
undergraduate/postgraduate elective as a part of the computer science and
engineering programme, and were introductory courses to NLP. The cohorts
consisted of undergraduate (nearly 50%) and postgraduate students.
Postgraduate students included those enrolled in Masters by Coursework or
Masters by Research programmes, and early PhD students.

The course components of NLP-UNSW and NLP-IITB, along with the course
conveners’ reasons behind covering classical approaches, are shown in Figures
1 and 2 respectively. Generally speaking, an exposition to classical
approaches allowed the students to solve problems and understand deep learning
approaches vis-á-vis their predecessors. NLP-UNSW insisted that the group
project compare deep learning methods with their predecessors. NLP-IITB
allowed the students to choose an appropriate method. In contrast, the
individual assignment in NLP-UNSW only involved using black-box NLP libraries
while NLP-IITB used multiple assignments covering both statistical as well as
deep learning models.

Figure 1: Course Structure for NLP-UNSW. Figure 2: Course Structure for NLP-
IITB.

##  3 Parallels to Computer Science Education

As NLP educators grapple with Classical-first, -later, or perhaps -interleaved
approaches to curricula, it is helpful to draw upon empirical research and
lessons learned by CS1 educators (introductory programming) who have grappled
with a similar dilemma: the age-long objects-first or -later debate. For
decades, introductory programming students learned imperative-style
programming in languages such as C, Pascal, and Fortran. In the early 2000s,
educators started incorporated object-oriented programming concepts into their
curriculum as object-oriented programming took hold in industry Cooper et al.
(2003). Where the objects-first community may begin immediately with concepts
of composition, inheritance, and abstraction, the objects-later community
instead focus on simpler, foundational programs and concepts such as sequence
and control flow.

The primary criticism of objects-first approaches surrounds the added
complexity necessary to discuss object-oriented concepts Proulx et al. (2002).
Objects-first must tackle objects, classes, encapsulation, and access
modifiers to discuss even the most basic object-oriented concepts. Of course,
objects-first educators will retort that this extra effort is worth it, with
students reporting a solid sense of program design and contextualisation of
object oriented concepts Cooper et al. (2003).

These criticisms of object-first approaches are not unfounded. We can apply
cognitive load theory, the theory of human cognition and how learning occurs,
to inform instructional design in computing and NLP. The theory, backed by
many empirical studies, finds that limited amounts of secondary information
(such as computing tasks) can be processed at any given time Sweller (2011).
Put simply, human cognitive architecture lends itself to learning best when
concepts are minimally introduced. This reduces the cognitive overload that
can hinder the assimilation of new information.

Cognitive load theory has been applied in introductory programming contexts,
finding that cognitive load measures and tools can be applied to computing
education to inform curriculum and instructional design Morrison et al.
(2014).

While cognitive load theory may, at first glance, support an objects-later
approach due to the reduction of concepts required, approaches to reduce
cognitive load when delivering objects-first curriculum may be preferable if
it aligns with its goals.

Empirical studies of learning outcomes between objects-first and -later seek
to focus on measurable evaluations of student learning outcomes. Ehlert and
Schulte (2009) found no differences in learning gain between objects-first and
objects-later courses; however, they did find that students in objects-later
courses reported lower perceived difficulty and higher comfort levels. (Tew et
al., 2005) compared objects-first/later at the same institution and found that
students performed comparatively by the end of their second term. A more
recent, large-scale systematic literature review on Introductory Programming
seems to support this nuanced take on programming paradigms Luxton-Reilly et
al. (2018). The authors find that there is still active research on
programming paradigms, and surmise with: “after full consideration of all the
papers it is by no means clear that any paradigm is superior to any other for
the teaching of introductory programming". We may glean from this comparison
to CS1 education design that many dimensions are involved in curriculum
design. Empirical studies have found that the goals of the program and the
institution itself, perspectives of educators, and quality of instruction and
instructional materials are more critical than an objects-first or -later
design.

Unlike CS1 education, however, NLP may often be available as a single elective
in a computer science program. Therefore, NLP educators are forced to balance
providing practical, deep learning skills to students while also providing
solid foundations in classical NLP in a shorter time-frame, perhaps supporting
an interleaved approach to NLP curricula.

Authors; Publisher |  Year |  Chapter Layout |  Deep learning focus
---|---|---|---
Speech and Language Processing; Dan Jurafsky, James H Martin; - |  2024 |  Fundamental Algorithms (Statistical Models, Neural Models, RNNs, LSTMs.) followed by NLP applications and linguistic tasks. |  Techniques first. classical: Yes.
A Course in Natural Language Processing; Yannis Haralambous; Springer |  2024 |  Layers of NLP: Phoneme, Grapheme, Morpheme. Last chapter: Going Neural. |  Neural Models (RNNs, Transformers)
Natural Language Processing; Pushpak Bhattacharyya, Aditya Joshi; Wiley |  2023 |  Fundamental techniques first. Then neural. Significant focus on NLP problems. |  Interleave classical and neural both. Three generations.
Real-World Natural Language Processing; Masato Hagiwara; Manning |  2022 |  Neural-focussed. Embeddings, SentenceClasification, Seq2Seq, Transformer, etc. |  Neural-focussed.
Deep Learning for Natural Language Processing; Stephan Raaijmakers; Manning Publications |  2022 |  Text embeddings, sequential NLP, attention, multitask learning, last chapter: Transformers and using Transformers. Lots of code examples |  Neural focussed.
Practical Natural Language Processing; Sowmya Vajjala, Bodhisattwa Majumder, Anuj Gupta, Harshit Surana; O’Reilly |  2020 |  NLP Primers: Quick introduction to primary NLP concepts. Very task driven: Classification, IE, Chatbots, Applications to domains |  Cover deep learning Early. Focus on applications and tasks
Introduction to Natural Language Processing; Jacob Eisenstein; MIT Press |  2019 |  Learning: Classification (Tasks and approaches); Sequences (Tasks and approaches); Semantics. Word embeddings, parsing, reference resoluton |  Pre-deep learning first. Then neural.
Table 1: Deep learning focus in some NLP textbooks listed in the reverse-
chronological order.

##  4 Observations from NLP textbooks and courses

Table 1 presents a summary of some NLP textbooks, in terms of layouts and
their deep learning focus. The books were identified using a search on the
UNSW library. The focus was identified using the content plan of the book,
along with a surface analysis of the chapters. We observe that nearly all
textbooks cover classical approaches, primarily in terms of statistical
models. We describe two textbooks in particular. The textbook by Jurafsky-
Martin 333https://web.stanford.edu/~jurafsky/slp3/ divides its chapters into
fundamental algorithms and NLP applications. The first five chapters introduce
regular expressions, one-hot vectors and statistical algorithms like support
vector machines and logistic regression. In the subsequent chapters, the book
covers word embeddings, then begins to combine LSTM with CRFs in the context
of POS tagging. Following that, the book covers Transformer, fine-tuning and
prompting/prompt learning Transformer. Bhattacharyya and Joshi (2023) use a
different approach. They cover fundamental algorithms for representation
learning: computational grammar, probabilistic language modeling, and
word2vec/LSTM-based representations. The book visualizes NLP as three
generations: rule-based, statistical and neural. Following that, the book
introduces Transformer. The subsequent chapters alternate between the
approaches in the three generations.

Table 2 illustrates how some NLP courses cover classical topics. We only use
examples of courses whose course outlines are publicly available on the
internet. Similarly, this is not a complete list either. In universities where
there is a deep learning-focused course for NLP, topics such as syntactic
parsing or statistical classification are covered in substantial detail. Even
for courses that cover little classical content, n-gram language modeling is a
topic that is included. The table also shows ‘when is Transformer taught’
which may be viewed as a turning point when deep learning-based approaches
assume focus in the course. We view Transformer as a transformative technology
in NLP, and do not claim that all of deep learning is Transformer.

University |  Year |  Examples of pre-deep-learning topics |  When is Transformer taught?
---|---|---|---
UMAss Amherst444https://people.cs.umass.edu/~miyyer/cs685/ |  2023 |  N-gram language modeling |  Week 2 of 11
CMU555https://phontron.com/class/anlp2024/course_details/ |  2024 |  Representing words |  Week 3 of 16
IIT Delhi666https://www.cse.iitd.ac.in/~mausam/courses/col772/spring2024/ |  2022 |  Finite state automata, statistical parsing |  End of month 2 out of 3.5
University of Edinburgh777http://www.drps.ed.ac.uk/23-24/dpt/cxinfr10078.htm |  2024 |  Lexical, syntactic and semantic parsing, etc. |  This only covers algorithmic fundamentals; separate course for neural models
University of Washington888https://safe-fernleaf-26d.notion.site/Winter-24-CSE-447-517-Natural-Language-Processing-4142333a001143d2be5ecff1a535c4ab |  2024 |  N-gram language modeling |  Week 2 of 11
NYU 999https://nyu-cs2590.github.io/spring2023/calendar/ |  2023 |  Feature-based classification, N-gram language modeling |  Week 3 of 15
Table 2: Examples of the coverage of deep learning in NLP courses.

##  5 Lecture Plan

Figure 3: Lecture Plan for NLP-UNSW.

NLP-UNSW: In the NLP-UNSW course which is spread over 10 weeks, we adopt a
hybrid methodology where we interleave deep learning approaches with
statistical/rule-based approaches. The hybrid methodology is illustrated in
Figure 3. In the first week, we introduce NLP via black-boxes such as spacy,
nltk, and HuggingFace pipelines. The students are introduced to NLP tasks with
demonstrations of the three libraries. This is to help the students develop an
understanding of the task. Similarly, if students aim to only ‘use’ NLP in
their projects (which may be sufficient for interdisciplinary projects), these
libraries are sufficient. The focus here is also to help them understand the
input and output of NLP systems, which we believe is the starting point to
understanding NLP.

In week 2, we cover representations of text via one-hot vectors and
probabilistic language modeling (statistical approach), and word
representation learning as in word2vec and GloVe (deep learning approach).
This not only allows students to appreciate the value addition of deep
learning approaches but also identify situations in which non-deep learning
approaches may be sufficient. In week 3, we focus on Transformer architecture:
exposing the students to the architectural details, pseudocode, and code
implementations. This is followed by Transformer-based models (encoder,
decoder, and encoder-decoder models) in week 4. With this background in neural
NLP models, we switch gears and focus on one NLP task every week. Every task
is covered using the following steps: the linguistic task and associated
challenges, classical approaches, deep learning approaches, and recent
advances in the area. The first two allow the students to gain a foundational
understanding of the problem, followed by the state-of-the-art in deep
learning. The recent advances are catered to students who might be interested
in future research in NLP without going into too much depth - to ensure that
the content is accessible. The NLP tasks we cover are: sentiment analysis
(representing sequence classification), named entity recognition (representing
token classification), machine translation (representing sequence-to-sequence
tasks), summarization (modified sequence-to-sequence tasks) and bias
mitigation.

In NLP-UNSW, we experience a recurring challenge when discussing NLP tasks
every week. Foundation models (both encoder-only and decoder-only models) are
versatile in their utility for different tasks. Therefore, we structure each
neural section in three steps: (a) fine-tuning BERT, (b) one or more advanced
methods relevant for the task. This serves two purposes. It allows us to teach
different fine-tuning techniques. In addition, it also permits us to ground
them in specific NLP tasks. We remember to remind students that the method is
applicable in other NLP tasks.

NLP-IITB: NLP-IITB starts with a focus on sequence labeling via HMM-based POS
tagging, followed by tree extraction via probabilistic parsing. In both cases,
the mathematical details (driven by probability) go hand in hand with the
algorithms (explained through the code). Then, machine translation is
introduced, which makes way for an introduction to Transformer and large
language models. The subsequent weeks discuss sentiment analysis as a specific
NLP task and evaluation metrics in NLP. It must be noted that NLP-IITB is the
introductory NLP course while there is a deep learning-specific NLP course at
IITB which is often a follow-up to the introductory NLP-IITB. This is not the
case for NLP-UNSW (being the only NLP-centric course). As a result, the course
needs to balance between the two. This comparison shows how educators may make
different choices, depending on the length of the teaching period. As a
result, the lecture plan of NLP-IITB uses the spectrum shown in Figure 4.
classical approaches allow focusing on the linguistic phenomenon which is
captured using a model. The data provides the parameters of the model.

Comparison: In both NLP-UNSW and NLP-IITB, however, we observe that the
foundational material serves as a good basis to introduce terminology (for
example, types of summarization are abstractive and extractive summarization)
and tag sets (as in the case of named entity recognition). The classical
approaches build an intuitive understanding of building computational models
for the specific NLP task. Appreciating the challenges in the classical
approaches leads the students to the need for deep learning approaches.
Through handwritten examples in the lecture, we highlight the relationships
between the mathematics of classical approaches and Transformer-based
approaches (for example, alignment model in statistical MT with cross-
attention in Transformer).

Figure 4: Lecture Plan for NLP-IITB.

##  6 Coding Assessments

Both NLP-UNSW and NLP-IITB have individual and group coding assessments. NLP-
UNSW has one of each, while NLP-IITB has two individual and one group
assessment(s).

###  6.1 Course Assignment

NLP-UNSW: The first coding assessment in NLP-UNSW is an individual coding
assignment completed by students by the end of week 3. The coding assessment
is run in a competition-like environment. The students are given a document
defining the problem definition, and a template code that also contains stubs
for testing. The students are required to add to the template. Closer to the
submission, the students are given test cases to evaluate their code. The
topic of the individual assignment needed deliberation. Until that point, we
have only started discussing Transformer in the lectures. Therefore, we
utilize the individual assignment to assess the classical skills of the
students. In the case of this offering, the task was to extract skills from
job ads, based on a skills ontology. The assignment was designed in two parts:
the first part required the students to use the spacy matcher, while the
second part required them to use embedding similarities. The former tests them
for their ability to use a classical library while the latter requires them to
use HuggingFace models. As a result, the assessment covers the students’
ability to ‘use’ NLP models. Marking the assignment includes an automatic
marking component with test cases and manual marking by the tutors. Being a
rule-based system, the evaluation of test cases is found to return low
precision. Therefore, rather than scoring on individual test cases, we mark
the students on precision thresholds.

NLP-IITB: NLP-IITB follows a similar strategy although there are multiple
individual assignments. The course convener found it useful to give classical
assignments on topics such as POS tagging, parsing and so on. An innovative
assignment was also tried out, which met with good student feedback. Given a
large dataset of names of cities, the task was to identify a preferred suffix
in the name of a city. Students reported multiple deep learning/non-deep
learning approaches.

###  6.2 Course Project

Running in its first year, NLP-UNSW provides detailed guidelines for the
course project. In contrast, NLP-IITB provides less guidelines but involves
periodic consultation with the course team.

NLP-UNSW: The group project is a centerpiece of the NLP-UNSW course, allowing
students to explore diverse topics within NLP. Teams of four to five students
are encouraged to select a specific area of interest, ranging from NLP topics
of active research such as prompt recovery in large language models to purely
applied topics like developing a virtual learning assistant using Retrieval
Augmented Generation Lewis et al. (2020). To guide students effectively, we
provide a detailed scope guideline document. The document outlines the
following key aspects alongside their respective credits (cr):

  1. 1.

Problem definition: Must be an NLP problem ($5$ cr) with a text-based
source/domain ($5$ cr);

  2. 2.

Dataset selection: Use an existing dataset ($10$ cr), create your own labelled
dataset ($20$ cr) and use an existing lexicon ($10$ cr);

  3. 3.

Modelling: Implement a rule-based/statistical baseline ($50$ cr), use an
existing pre-trained model ($5$ cr), fine-tune your own model ($50$ cr), and
integrate a language model with external tools ($20$ cr);

  4. 4.

Evaluation: Quantitative ($10$ cr), qualitative ($5$ cr), command-line testing
($5$ cr) and demonstration ($10$ cr).

Project teams are expected to cover a minimum of 100 credits. The aspects show
that, while deep learning-based techniques, carry a significant focus,
students are encouraged to experiment with simpler models.

#### Project evaluation.

The submission evaluation is structured around specific questions that capture
the essence of a well-rounded NLP project pipeline. These include the
evaluation of the project report – for scope: architectural, methodological,
and analytical details; group presentation – for quality: architectural
details, presentation format/style; codebase – for code style: readability,
scope, errors, and structure, and individual effort of group members. For the
lattermost evaluation, each group is to submit an individual contribution file
enlisting the technical contributions of each member.

#### Findings.

The diversity of modeling algorithms is particularly interesting across the
submissions (see Fig. 5). We note that classical techniques such as such as
lexicon-based systems, traditional machine learning algorithms (e.g., SVM,
Naive Bayes), and feature engineering-based techniques serve towards
foundation building, interpretable analyses, and resource efficiency all while
allowing the students to appreciate the advancements brought about by deep
learning in NLP by benchmarking against them. Deep learning models (Fig.
5(a)), on the other hand, help achieve complex pattern recognition, state-of-
art performance, and end-to-end learning while helping the students understand
the laws of scalability on large-scale datasets.

(a) Deep-learning

(b) classical

Figure 5: Word clouds showing the key deep learning and classical methods
explored in the group projects.

NLP-IITB: In NLP-IITB, we list a few topics for students to choose from, while
being open to new ideas. Providing topics helps to streamline project ideas
while giving student teams a headstart. The projects are evaluated using a
combination of demonstration and presentation, including an in-person
discussion with the course team. The focus is the selection of the ‘right’
algorithm. The difference in the level of detail appears to reflect the
experience of the two academics running the courses.

###  6.3 Tutorials

Tutorials are a weekly activity in NLP-UNSW (while not a part of NLP-IITB). In
a typical tutorial, we first cover a focused review of the content covered in
the lectures. We initially provide a brief overview of classical methods, as
these approaches often greatly assist students in understanding the task.
Among the classical topics, students show interest in learning about POS
tagging and HMM-related algorithms. In the tutorial, we emphasize the
mathematical derivation of HMM itself to improve the student’s understanding.
Subsequently, we extend the discussion by integrating the latest research
related to the lecture topics. This part is focused on expanding on the
lecture content to cover recent, trending papers that are not included in the
syllabus. For instance, when discussing Parameter-Efficient Fine-Tuning
(PEFT), we incorporate a paper-reading session of the paper by He et al.
(2021), explaining its essence from a unified perspective and how it can be
generally summarized. This allows us to meet the expectations of students who
may be interested in advanced topics. Next, we utilize code demonstrations to
illustrate the concepts presented in the lectures, facilitating a deeper
understanding for the students. Following this, we explain and demonstrate the
coursework requirements, such as homework assignments. Finally, we conclude by
addressing student questions, which may pertain to projects or other
assignments. Particularly in the tutorials, the students show less interest in
the classical sections, focusing more on deep learning-based methods that are
perceived as more employable. Students who actively participate and show
interest in the derivation of various model principles are often also
interested in research.

##  7 Making the Case for Classical Approaches

Based on the considerations discussed so far, we are now able to make several
arguments that may influence the inclusion of classical approaches in NLP
courses. Designing a curriculum based on course expectations along these
arguments may help determine the ‘balance’ that is the focus of this paper.

Figure 6: Intuition-building using classical approaches.

###  7.1 Intuition-building

The conveners of NLP-UNSW and NLP-IITB find that rule-based and statistical
approaches are great for intuition building and also appreciate that NLP is
challenging. Classroom exercises where students describe rules for a
particular NLP task enable them to see why a good rule-based system would be
laborious due to the well-known high-precision-low-recall setup. Statistical
approaches help to highlight the importance of probability in NLP. Probability
is the cornerstone of NLP models, including modern models. Softmax being the
center of Transformer-based models is an example of that. Starting with Bayes
theorem, a teacher can effectively tease out dependencies between different
variables, serving to be a great explanation to lead to attention and related
concepts, especially during lectures.

A pre-course survey done in NLP-IITB revealed that, out of 150 students, 80%
preferred that the course build intuition as opposed to providing information.
Information refers to providing a suite of approaches and methods, while
intuition refers to the motivation (linguistic or mathematical, etc.)
underlying the methods. In fact, both courses combine the pillars illustrated
in 6. Linguistics motivates the problem, probability and code run as common
threads allowing a comparison between the two kinds of approaches. This
motivation is highlighted by the instructor of NLP-IITB, by leveraging
examples from his rich research experience. In contrast, the instructor of
NLP-UNSW prefers to give examples from industry applications, given their
professional experience in the tech industry.

###  7.2 Student Motivation

Several blog articles on NLP are available online. A clear differentiator in a
university-based course is inspiring students using blended learning Deng and
Yuen (2010). Towards this, classical approaches are effective in inspiring
students to take up NLP projects. The conveners of NLP-UNSW and NLP-IITB
observe that the challenges of rule-based systems are clear with some
examples, during lectures. Covering classical approaches serves as a good
motivator for students to see why deep learning approaches have been
revolutionary to the field. This feeling of inspiration is often reported in
NLP-IITB.

###  7.3 Popular classical approaches

Classical approaches have done well for linguistic tasks, particularly at the
lower levels of the NLP hierarchy. Approaches like HMM and CRF work well for
POS tagging and other token classification tasks. We observe that past courses
also tend to cover classical methods as an introduction to deep learning
methods. Comparison of popular classical approaches with deep learning
approaches can aid learning during projects and assignments, as described in
Section 6.

###  7.4 Annotation

Classical techniques, particularly in terms of annotation, are the benchmark
for modern NLP models since tag sets used in classical approaches are still
useful for their linguistic rigour. An example is the POS tagset. Nuances in
Penn TreeBank about tags for “JJ" versus “JJR" (adjectives and comparative
adjectives) help the students understand why they were designed in a certain
way. The pre-course survey in NLP-IITB revealed that 67% students preferred
fundamental approaches versus state-of-the-art. The course covered a
combination of the two.

###  7.5 Cognitive load theory

Classical techniques often involve explicit, well-defined rules and simpler
models that can be more transparent and interpretable than their neural
counterparts. This clarity can reduce extraneous cognitive load for learners
by providing simpler examples of how inputs are transformed into outputs. For
instance, a decision tree for language processing allows learners to see the
exact paths through which decisions are made, thus aligning with the
segmenting principle of cognitive load theory.

##  8 Conclusion

Classical approaches for NLP refer to those prior to the predominant use of
neural networks and deep learning. This paper investigated the role of
classical approaches in an introductory NLP course, by comparing perspectives
from two courses: one which was offered for the first time and another which
has been running for nineteen years while being continually revised. We
discussed key considerations and reasons why classical approaches may be
helpful, in terms of the past textbooks, lectures, and assessments. An
understanding of classical NLP not only builds a strong foundation for the
students but also enables them to look back at some of these methods to
develop new techniques. We hope that the analyses presented in the paper will
allow NLP educators and students alike to find the right balance between the
classical and deep learning approaches.

## Limitations

The books and courses described in the paper are a subset curated only as an
example. It does not represent a complete list. Similarly, the sections derive
from insights teaching the two courses covered in the paper, and are not
necessarily prescriptive.

## Ethical Considerations

The paper describes summary statistics of student surveys without identifying
individual students or student cohorts. The assessment section provides only a
high-level view of the assignments and lectures, and may not result in
implications to academic integrity in the future versions of the courses.

## Acknowledgment

The authors thank Dipankar Srirag, UNSW Sydney, for his feedback on a near-
camera-ready draft of the paper.

## References

  * Bhattacharyya and Joshi (2023) Pushpak Bhattacharyya and Aditya Joshi. 2023.  _Natural Language Processing_.  Wiley.
  * Cooper et al. (2003) Stephen Cooper, Wanda Dann, and Randy Pausch. 2003.  Teaching objects-first in introductory computer science.  _ACM SIGCSE Bulletin_ , pages 191–195.
  * Deng and Yuen (2010) Liping Deng and Allan HK Yuen. 2010.  Exploring the role of academic blogs in a blended community: An integrative approach.  _Research and Practice in Technology Enhanced Learning_ , 5(02):53–71.
  * Ehlert and Schulte (2009) Albrecht Ehlert and Carsten Schulte. 2009.  Empirical comparison of objects-first and objects-later.  _ICER’09 - Proceedings of the 2009 ACM Workshop on International Computing Education Research_ , pages 15–26.
  * Foster and Wagner (2021) Jennifer Foster and Joachim Wagner. 2021.  Naive Bayes versus BERT: Jupyter notebook assignments for an introductory NLP course.  In _Proceedings of the Fifth Workshop on Teaching NLP_ , pages 112–114, Online. Association for Computational Linguistics.
  * Gaddy et al. (2021) David Gaddy, Daniel Fried, Nikita Kitaev, Mitchell Stern, Rodolfo Corona, John DeNero, and Dan Klein. 2021.  Interactive assignments for teaching structured neural NLP.  In _Proceedings of the Fifth Workshop on Teaching NLP_ , pages 104–107, Online. Association for Computational Linguistics.
  * He et al. (2021) Junxian He, Chunting Zhou, Xuezhe Ma, Taylor Berg-Kirkpatrick, and Graham Neubig. 2021.  Towards a unified view of parameter-efficient transfer learning.  In _International Conference on Learning Representations_.
  * Lewis et al. (2020) Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, et al. 2020.  Retrieval-augmented generation for knowledge-intensive nlp tasks.  _Advances in Neural Information Processing Systems_ , 33:9459–9474.
  * Luxton-Reilly et al. (2018) Andrew Luxton-Reilly, Simon, Ibrahim Albluwi, Brett A. Becker, Michail Giannakos, Amruth N. Kumar, Linda Ott, James Paterson, Michael James Scott, Judy Sheard, and Claudia Szabo. 2018.  _Introductory programming: A systematic literature review_.  ACM.
  * Morrison et al. (2014) BB Morrison, B Dorn, M Guzdial of the tenth annual conference on …, and undefined 2014. 2014.  Measuring cognitive load in introductory cs: adaptation of an instrument.  _Proceedings of the tenth annual conference on International computing_ , pages 131–138.
  * Plank (2021) Barbara Plank. 2021.  From back to the roots into the gated woods: Deep learning for NLP.  In _Proceedings of the Fifth Workshop on Teaching NLP_ , pages 59–61, Online. Association for Computational Linguistics.
  * Proulx et al. (2002) Viera K. Proulx, Jeff Raab, and Richard Rasala. 2002.  Objects from the beginning - with guis.  _Proceedings of the 7th annual conference on Innovation and technology in computer science education_ , pages 65–69.
  * Sweller (2011) John Sweller. 2011.  Cognitive load theory.  _Psychology of Learning and Motivation - Advances in Research and Theory_ , 55:37–76.
  * Tew et al. (2005) AE Tew, WM McCracken, M Guzdial Proceedings of the first, and undefined 2005. 2005.  Impact of alternative introductory courses on programming concept understanding.  _dl.acm.orgAE Tew, WM McCracken, M GuzdialProceedings of the first international workshop on Computing education research, 2005•dl.acm.org_.


# A Spin-based model checking for the simple concurrent program on a
preemptive RTOS

Chen-Kai Lin  Institute of Information Science, Academia SinicaTaipeiTaiwan
<EMAIL_ADDRESS>,  Ching-Chun (Jim) Huang  Department of Computer Science
and Information Engineering, NCKUTainanTaiwan<EMAIL_ADDRESS>and  Bow-
Yaw Wang  Institute of Information Science, Academia SinicaTaipeiTaiwan
<EMAIL_ADDRESS>
###### Abstract.

We adapt an existing preemptive scheduling model of RTOS kernel by eChronos
from machine-assisted proof to Spin-based model checker. The model we
constructed can be automatically verified rather than formulating proofs by
hand. Moreover, we look into the designs of a Linux-like real-time
kernel–Piko/RT and the specification of ARMv7-M architecture to reconstruct
the model, and use LTL to specify a simple concurrent
programs–consumer/producer problem during the development stage of the kernel.
We show that under the preemptive scheduling and the mechanism of ARMv7-M, the
program will not suffer from race condition, starvation, and deadlock.

model checking, concurrent program, preemptive scheduling

††copyright: none††doi: ††isbn: ††journalyear: ††booktitle:

##  1\. Introduction

Model checking (Clarke et al., 1999; Clarke, 2008) is first introduced by
Edmund Clarke and Allen Emerson in 1981 to solve the Concurrent Program
Verification. It has a state-transition graph (denote as a model) and some
logic formulas (denote as properties). The algorithm of model checking will
try to claim that all paths of the model are satisfied the properties. In
other words, if we write a property about mutual exclusion and the model
checker says the property is unsatisfied, we can trace the error messages back
to the situation and inspect whether the model or the real-world system will
suffer from the race condition.

Concurrent errors are hard to detect by code review or test case, because we
can not guarantee the asynchronous processes executing in a specific order.
Another way to ensure the correctness of concurrent programs is by proof, one
example is that Lamport proves the correctness of a fast mutual exclusion
algorithm in 1987 (Lamport, 1987). But, this strong guarantee requires the
preliminary of proof tactic and constructs by hands. Model checking, though,
has weaker guarantee but is more expeditious only if the abstract model and
the real-world system are homogeneous. Furthermore, the correctness of the
algorithm can not stand for the correctness of the implementation on other
hardware or software mechanisms, i.e. interrupt or softirq. Holzmann
(Holzmann, 2014) indicates model checking is one of the three topics that the
Mars Science Laboratory (MSL, launched by NASA) has used to reduce risk in
complex software systems. He also points out that they had successfully
verified several concurrent issues on key parts of the spacecraft, including
Cassini, Deep Space One, and the Mars Exploration rovers.

Piko/RT (Huang et al., 2018), developed at National Cheng Kung University, is
a non-trivial operating system but small enough for verification purpose. One
of the key features is real-time capability. It enables interrupts
(exceptions) almost all the executing time to handle the incoming IRQs.
Moreover, it is optimized for the ARM Cortex-M series. Until 2015 (Burr,
2016), ARM had shipped 20.6 billion Cortex-M units within six years and the
number is growing. It is hard to debug if such a number of devices deployed
around in different areas. Not to mention the software system must not behave
unexpectedly in the critical usages.

In this paper, we address the problem of verifying the simple concurrent
programs will not act unexpectedly (no race condition, starvation, and
deadlock) under the specific conditions (preemptive scheduling and interrupt-
driven mechanisms). We first construct an abstract model on the Spin model
checker based on three domains: proof framework of eChronos, source code of
Piko/RT, and reference manual of ARMv7-M, discussing in section 3. Next, write
three properties (race condition free, starvation free, and deadlock free) and
verify in Spin (section 4 and 5). Last but not least, discuss the background
knowledge and summarize the conclusions in section 2 and 6. All our
model111https://github.com/kaizsv/pikoRT-Spin.git is in the public domain.

##  2\. Background

We use Spin as our model checking tool and build an abstract scheduling model
on. In this section, we discuss some topics about Spin model checker and the
real-time scheduling before approaching to the model. And then, talk about
several related works of this paper.

###  2.1. The model checker

####  2.1.1. Spin

(a)

(b)

Figure 1. Example of $\omega$-automaton

Spin (Holzmann, 2018; Ben-Ari, 2008; Holzmann, 2003) is an open-source
verification tool of multi-threaded software developed in the Computing
Science Research group of Bell Lab. The theory behind Spin is the
$\omega$-automaton, which is the variation of classic finite state automata
with acceptance conditions on infinite executions. Consider Figure 1a, note
that the termination of the automata would not necessarily be a desirable
result. We can declare some state that will be visited infinitely often by
labeling accept, i.e. Run state, as a legal run. Because the states are
finite, the infinite run ($\omega$-run) will anyway repeat itself at the
certain degree just like Figure 1b shows. If Spin find an $\omega$-run with
some state labeling accept, it can claim that the automata is accepted. This
is so called the Büchi acceptance.

Every thread in Spin is an automata and product altogether in the verifying
stage. Spin supports a meta language: PROMELA, which interpreting readable
script into automata, like common condition statements, if or do. It also
provides channel allowing the communication between two threads. And the most
important one in this paper is the guard. guard is a true of false expression
that guard the execution of the following statements only if it is true,
otherwise the thread will be blocked until it becomes true.

####  2.1.2. Linear temporal logic

Safety and liveness. We need to discuss these two kinds of properties before
going to linear temporal logic, which are introduced by Lamport in 1977
(Lamport, 1977). Safety property guarantees nothing bad ever happens, e.g.,
more than two processes access same critical section at the same time will
never happen. Liveness property denotes as something good eventually happens,
e.g., if a process wants to enter its critical section, it can eventually
enter. Above is only the informal expression of two types of properties.

Fairness is another issue of temporal logic. We can not assume relative speeds
of asynchronous processes, there might exist a run that when a process can
execute, but never be executed. This is called the unfair processes. Two
commonly used variants of fairness are:

weak fairness: If a statement is continuously enabled, it will eventually be
executed
strong fairness: If a statement is enabled infinitely often, it will
eventually be executed

Figure 2. Semantics of Global and Future operators

Temporal logic allows us to formalize the properties of a run unambiguously
with some special operators. Most relevant to the verification of asynchronous
process systems is a specific branch of temporal logic, linear temporal logic
(LTL). LTL is sufficient to describe two operators in the scope of this paper.
Let $f$ be a LTL formula. Operators in $f$ such as not, and, or, implication,
and equivalence are still a LTL formula. Two further temporal operators global
and future are introduced below and Figure 2:

$\Box f$: $f$ is true now and forever in rest of the run
$\Diamond f$: $f$ is true eventually in the future run

Figure 3. Mutual exclusion

Let us consider an example of mutual exclusion. Figure 3 contains two
processes and CS is the critical section of that process. Each process is
first in non-critical section. If one process wants to access its shared
variables in critical section, it must try to gain lock first at Try-CS state
and leave the critical section as soon as possible. We can write down the LTL
formula about mutual exclusion free, starvation free, and deadlock free as
follows:

mutual exclusion free: $\Box\neg(\text{CS}_{1}\wedge\text{CS}_{2})$
starvation free: $\Box\Diamond\text{Try-
CS}_{1}\rightarrow\Box\Diamond\text{CS}_{1}$
deadlock free: $\Box\Diamond(\text{Try-CS}_{1}\wedge\text{Try-
CS}_{2})\rightarrow\Box\Diamond(\text{CS}_{1}\vee\text{CS}_{2})$

The first property is simple. Both processes can not access its critical
section at the same time in every state of a run. The rest are the liveness
properties. Starvation free means if a process try to enter its critical
section infinitely often, it will be in critical section infinitely often. And
deadlock free property means if both processes try to enter each critical
section infinitely often, at least one process can enter its critical section
infinitely often. Note that “infinitely often” represents the properties are
strong fairness. This is will be discuss later in section 4.

To understand how Spin verifies LTL formula, consider it as a game. Spin
negates the LTL formula and converts it into never claim. The never claim is
also an automaton that can product together with the model. The Spin model
checker then try to find a path that satisfied the negated formula which means
there exists a counterexample in the model that violates the property. On the
contrary, if never claim never reaches the acceptance state (never finds a
path that violates the formula) means the model satisfied the formula.

###  2.2. Real-time scheduling

A real-time system is a set of tasks which running interleaving on
uniprocessor or concurrently on multi-processors that can simply classify into
preemptive and non-preemptive scheduling. Non-preemptive scheduling has lower
context switch latency but the interrupt handler might violate the deadline.
And preemptive scheduling forces each task to process under a limited time and
the task might be blocked (pending) even if within its timeslice. In this
section we discuss several factors which affect the behavior of preemptive
scheduling from the hardware and software aspects. The hardware is the
mechanisms of ARMv7-M architecture and the software is the implementation of
the case study.

####  2.2.1. Exception of ARMv7-M architecture

ARMv7-M architecture (ARM Limited, 2014; Yiu, 2013) uses “exception” as a
response to system event and “interrupt” as a peripheral request. Exception
(or interrupt) with higher priority level can preempt the lower one. Moreover,
synchronous exception like non-maskable interrupt (reset, hardware fault),
system fault, and SVCall must execute before the context switch. This means
synchronous exception can only be preempted by higher priority level exception
before changing to the next task. The incoming exception will be pending if
the priority level is less than or equal to the current one. Other exceptions
are considered asynchronous that we can not guarantee the timing of executing,
even after the context switching.

Exception entry and exception return are the mechanism before and after the
exception handler take place on ARMv7-M architecture. While an exception
occurs, the hardware will compare the priority of current task and the coming
exception. The exception entry will push parts of the context into the stack
and reset return values of current context if the coming exception is allowed
to preempt according to the interrupt policy. After finishing the handler
task, the exception return will choose a proper task (from the stack or the
pending state) to switch to.

Tail-chaining is the further extension of the exception return. Tail-chaining
can continue to process the pending exception at the exception return stage.
Rather than restoring to the return context from the stack and saving it back
again to the stack, tail-chaining can directly switch to the pending exception
with less timing gap.

Context switch is a significant issue in this paper. Context switch typically
requires processor to execute at a critical region of interrupt disabled to
avoid the corruption of data during the switch, However, the busy waiting
might cause pending the coming exception and violate the deadline. ARMv7-M
supports interrupt enabled context switch. SVCall is a synchronous exception
and triggered by the svc instruction from user tasks to perform supervisor
call. PendSV is an asynchronous software interrupt and handles the scheduling
point enabled by the systick handler. To enable interrupt during context
switch, the ARMv7-M reference manual suggests to configure both exceptions
with the lowest priority level so that they can not preempt each other.

####  2.2.2. Preemptive scheduling

Preemptive scheduling causes the task to stop and resume executing frequently.
One reason is the task reaches its timeslice and does not finish yet, the
scheduler need switch to the next task from the runqueue. Another reason is
when a task with higher priority added into the runqueue, at any scheduling
point the system needs to guarantee the priority of current task is always the
highest one in the runqueue. The following lists several aspects which will
influence the behavior of the preemptive scheduling.

Bitmap scheduler has 32 priority levels and two priority arrays, active and
expired, which can be swapped in constant time. The scheduler always chooses
the highest priority task from the active priority runqueue and selected in
round-robin way if multiple tasks exist in the same priority level. The
implementation of array data structure and the bitwise operations make time
complexity in constant time.

Softirq and tasklet. Interrupt handlers are asynchronous and often timing-
critical so there are several limitations, such as respond rapidly and cannot
be blocked. Softirq is the mechanism that moves the execution of the non-
critical job (bottom half task) from interrupt handlers to the user task
(softirq process). Moreover, softirq maintains a bitmap scheduler with only
one runqueue to manage the different bottom half tasks, called tasklet.

Mutual exclusion is one of the solutions to prevent race condition and has
different implementations. In this paper, we focus on a pair of load-
link/store-conditional instructions, ldrex and strex, supported by a state
machine exclusive monitor provided by ARMv7-M architecture. Each processor has
a exclusive monitor called local monitor (we only consider uniprocessor
situation here), which will mark a segment of memory address (register) as
exclusive by the calling of ldrex instruction. One local monitor can only mark
one register at the same time, ldrex will load a value from the address to the
register and clear the previous mark and mark the address as exclusive. strex
conditionally stores the value back to the address if the address is marked as
exclusive and clear the mark at the same time, otherwise the store will fail
notifying by the return value. In brief, no matter how many times ldrex mark
the address, only one can update the value of that address by strex. And
finally, all mark will be cleared at every exception return stage. This make
sure the atomic operations of the mutex variables.

Condition variable is an extension of mutual exclusion. It will temporary
release the lock and move itself out of the runqueue if the condition is not
satisfied (condition wait). While others get the lock and satisfy the
condition statement, it signals the blocked one by returning the lock and
enqueuing the blocked one again (condition signal). This is more efficient
than busy waiting because the blocked one will temporarily gives up the
processor’s resources and turns to the process.

###  2.3. Related work

eChronos (Andronick et al., 2016) is a tiny real-time OS running on ARM
Cortex-M3 platform developed by Data61 in Australia. They provide a framework
and prove the property “the running task is always in the highest priority” on
the Isabelle/HOL proof assistant based on the Owicki-Gries (Owicki and Gries,
1976) method. The OG method is the parallel version of Hoare logic, known as
the pre- and post- condition style, guaranteeing the shared variables are not
interleaving by the parallel programs. Their framework is delicate and
scalable that simulates both software and hardware behaviors in one model. But
the challenge of their work is the exhausting hand constructed proof and the
lack of implementation details. The reason of the later one is the proof
strategy that they do not declare the explicit interrupt policy, causing all
exceptions can preempt each other. Instead, they have proved a larger range of
the exception behavior is correct that can implicate to the limited and real
one.

OSEK-Spin, Zhang, et al. (Zhang et al., 2015) use Spin to verify the
application of a standard automobile OS, OSEK/VDX, which is widely adopted by
many automobile manufacturers. To enhance the user experience, different
applications are developed based on the OS. To check whether the applications
can run correctly, the researcher provide a Spin-based model that can
replicate the executions on OSEK. The correctness means under the concurrent
running task, synchronous event, and context switch, the user application will
not suffer from race condition or priority inversion. They also developed
bounded model checking to verify more complex applications. However, the model
considered only the software aspect and did not contain the specific hardware
behavior.

The two researches list above are the most related to our paper. Moreover,
there are lots of corresponding work about verifying software or hardware by
mathematical proof, for example, seL4 (Klein et al., 2009). However, the
design of seL4 kernel is optimized for the formal verification, there are some
limitations. Although seL4 had analyzed the WCET (Blackham et al., 2011), its
kernel code only has few interrupt points, others with interrupt disabled.
This is different from the common design of RTOS.

##  3\. The model

Figure 4. The schema of the model (2 user tasks, 2 interrupts)

In section 2, we had discussed several factors of scheduling. In this section,
we show how we model those factors by PROMELA. The model consists of three
static processes (SVC, PendSV, and softirq) and an amount of user tasks and
interrupts (number of interrupt must contain one systick). Figure 4 is a
schema of 2 user tasks and 2 interrupts. The model can separate into three
parts: user task for the orange box, exception for the blue one, and two
special exceptions SVC and PendSV for the green one. Each process has a PID
listed at the top of Figure 4.

###  3.1. Overview

We had mentioned that each process are executed in asynchronous order, we use
this feature to simulate the incoming of the IRQs. But to determine which
process is the legal one to occupy the resource of processor, eChronos
introduced a guard called AWAITS to control the executing of the processes.
Another variable AT (active task) records which process is the legal on to be
executed. Every statement in the model will be wrap by AWAITS and can be
executed only if the AT becomes its PID, otherwise, the statement will be
blocked until AT becomes its PID again. There is also an A_AWAITS statement
which do the same thing as AWAITS, because there are two atomic statements in
PROMELA, d_step and atomic. Both statements guarantee no other processes can
interleave within the scope of the statement. The difference is that in
verification stage, the d_step is seen as one step while the atomic is depend
on the statements inside. Note that each statement in the code segment
surrounding by a frame is wrapped by the AWAITS or A_AWAITS statements which
are the unit operation in our model.

Starting from SVC handler first, we modeled five system calls, including,
mutex lock, mutex unlock, condition wait, condition signal, and pthread yield.
Consider that SVC is synchronous, we use a synchronous channel called
rendezvous channel in PROMELA to perform the behavior of calling the system
call. It is something like the client/server model that the SVC handler is the
server and serves several user tasks. The difference is that other processes
remain blocked during the communication. Recall the interrupt enabled context
switch, PendSV is asynchronous and used to respond the scheduling request from
the systick. Simultaneously, the systick handler will insert its bottom half
task into the tasklet runqueue waiting to be executed in softirq process.
Another interrupt handler do nothing in the model. Last, we choose the classic
consumer/producer program as our application to verify and the softirq will
discuss later.

###  3.2. Exceptions of ARMv7-M architecture

Figure 4 shows that every exception is starts with ITake or PendSVTake and
ends with IRet (except SVC is synchronous) which models exception entry and
exception return. There are two situations in ITake. First, we refer to the
manual of ARMv7-M to implement the interrupt policy, including the priority
and the pending state to determine whether the incoming IRQs can preempt the
current process. PendSVTake is a simplified ITake and only affects to the
PendSV process. An array ATStack stores the preempted processes that has not
finished its job yet. IRet elects the next running task from the top element
of ATStack or the highest priority of pending state when the current interrupt
handler is finished. If the exception priority of the top of the ATStack is
higher, pop the exception directly to the AT. If not, remember that the
exception in pending state has not been executed yet, an additional variable
ghost_direct_AT is introduced to record this situation and can be detected by
the second condition of ITake. The choosing of pending state running first is
similar to the tail-chaining mechanism in ARMv7-M

The design of ATStack is an array data structure that the last element in it
must be user task, others are exceptions in priority order. The formalization
of context switch is to change the last element in ATStack. Because context
switch only occurs in SVC or PendSV processes, the only element in ATStack
must be current user task and the AT must be the PID of SVC or PendSV. We add
several assert to check this scene and change the last element in ATStack to
reproduce the behavior of context switch.

###  3.3. Preemptive scheduling

Two priority runqueues, which contain an unsigned map and a queue, form the
structure of bitmap scheduler. One key difference between the model and the
source code is the swap of two priority runqueues. The source code uses
pointer to swap each other, however, the model uses bitwise operations to do
that. Two priority runqueues sched_bm[2] are defined in the model. Another
global bit SCHED_STATE_SWAP is helped to distinguish each runqueue. To swap
the runqueues, just xor the swap bit. Additionally, the ACTIVE and EXPIRED
thread state are designed in the same way.

ACTIVE: $(0|\text{SCHED\\_STATE\\_SWAP})$
EXPIRED: $(1\oplus\text{SCHED\\_STATE\\_SWAP})$

In short, the softirq is a user process which executes the bottom half task of
the interrupts. And the tasklet is a one priority runqueue managing which
bottom half tasks take place first. If no more bottom half task can be
executed, the softirq process will give up the processor’s resource by calling
the pthread yield system call. But notice that if the softirq has higher
priority than other user processes, the system call still choose softirq as
next process.

The lock and unlock of mutex can split into two stages: non-privilege and
privilege because of the supporting of load-link/store-conditional (LL/SC)
instructions. Take mutex lock for example, if the lock is free then gain lock
directly in the non-privilege mode by the mechanism of LL/SC, otherwise,
calling the mutex lock system call to give up the execution (moving itself out
of the runqueue). Another point to note that, there must have a place to store
the tasks moving out of the runqueue by mutex. The implementation of the
source code is a linked list structure, we use an array structure in PROMELA,
instead. However, to reduce the size of the model, there is only one slot in
the array currently and scalable depending on the applications.

Implementation of condition variable is based on the mutex that will
temporarily release the lock and gain lock again if the condition is
satisfied. Nonetheless, this is difficult to implement in PROMELA. In source
code, every process performing context switch in SVC or PendSV handlers which
will stop at a specific point in the handler and resuming when switching back.
If we want to emulate this behavior in PROMELA model, the SVC and PendSV
handler must duplicate times of the number of user task. This is a great
effort for model checking that we need to share the SVC and PendSV handler
within each user task. This leads to another problem that we can not place two
scheduling points in one exception handler and the scheduling point must
establish just before the IRet. This limits the modeling of condition wait
system call that we need to use two system calls (condition wait and mutex
lock) and wrap together with atomic statement to complete the one system
call’s job.

##  4\. Strategy of verification

Table 1. Options of Spin model checker Spin Version 6.4.8 - 2 March 2018
---
| Spin options | Verification options | Runtime options
Safety properties | -a |  -DXUSAFE, -DCOLLAPSE, | -m100000000
|  |  -DSAFETY, -DNOCLAIM, | (-m<changeable>)
|  | (-DMA=24), -DNOFAIR, |
|  | -DMEMLIM=<changeable> |
LTL acceptance |  -a, |  -DXUSAFE, -DCOLLAPSE, |  -m100000000,
cycles | -DLTL | (-DMA=24), -DNOFAIR, |  -a,
|  | -DMEMLIM=<changeable> | -N <ltl name>

We had talked about the model, now discussing the properties and how we verify
the model by Spin model checker.

###  4.1. The properties

These two methods are used to verify the correctness of the model:  i)
assertfor safety property,  ii) LTLfor liveness properties.  The assert is not
only the safety property but also a useful tool to check whether the model is
correct during the process of modeling. We use assert in the following ways.

  * •

The insertion of the queue will not induce buffer overflow and the deletion of
the queue must succeed.

  * •

If the value of map is not zero, there must be some elements in the queue.

  * •

If the scheduler chooses idle as next thread, the current thread must not be
idle.

  * •

The modification of IRQ pending state must be the interrupt process.

  * •

The tail-chaining only happens when no other exception priority in pending
state is higher than itself.

  * •

The ATStack will not have buffer overflow.

  * •

PendSV can only preempt the user task.

  * •

The consumer/producer will not suffer from race condition using two global
bits cs_c and cs_p to record the entrance of critical section.

  * •

Only user tasks can perform the system call when there is no pending
exception.

  * •

Only user tasks can perform context switch when there is no other active
exception (excluding SVC and PendSV).

  * •

The last element in ATStack is a user task; others are UNKNOWN222ARMv7-M
resets the register with UNKNOWN value during the context switch.

  * •

Mutex list (array) must not be empty if the value of mutex is larger than
zero.

  * •

The value of mutex must not smaller than -1.

For LTL, we label the condition loop as want, it means that the process wants
to enter its critical section but blocked at the condition loop. The $@$
symbol means the execution is at the statement with specific label. Note that
we apply the strong fairness in the LTL formula. If not, the model checker
will consider the situation that the systick preempt itself forever. But this
is impossible that the duration of systick is 1ms in the real-world system.

consumer starvation free:
$\Box\Diamond\text{consumer@want}\rightarrow\Box\Diamond\text{cs\\_c}$
producer starvation free:
$\Box\Diamond\text{producer@want}\rightarrow\Box\Diamond\text{cs\\_p}$
deadlock free:
$\Box\Diamond(\text{consumer@want}\wedge\text{producer@want})\rightarrow\Box\Diamond(\text{cs\\_c}\vee\text{cs\\_p})$

###  4.2. Spin options

The hardware environment in this paper is a 1TB memory machine with Xeon 6134M
3.2GHz processors. Table 1 is the Spin options for Safety and LTL
verifications. The search algorithm in this paper is the DFS. Looking at Spin
options first, -a is needed to generate the verification code and -DLTL is a
custom macro that used to load the LTL properties. In Verification options,
-DXUSAFE, -DCOLLAPSE, and -DNOFAIR are used in both properties, the first one
is to disable the usage of xr and xs assertions, the second one is to compress
each state to reduce the memory usage, the third one is to disable the weak
fairness provided by Spin (we use strong fairness in LTL formula). -DNOCLAIM
is to disable the usage of never claim, but enables while verifying the LTL
properties. -DSAFETY is used in safety property only. -DMEMLIM is the maxima
memory that Spin can use and -DMA is the algorithm of minima automata which
saving the memory but spending lots of running time. Next, the -m<changeable>
is the maxima depth for the DFS algorithm and -N used to choose which LTL
property to verify.

Spin model checker will provide statistics if the verification is completed
under the memory and maxima depth boundary. It also provides a list of
unreached statements in the model but never be executed. To analyze this list,
there are eight scheduling points in the model. We copy the macro of
scheduling points eight times with different names. With this setting, we can
tell the difference between the eight scheduling points by the different lines
of code and analyze them later.

##  5\. Discussion

We verify a classic concurrent program–consumer/producer in this paper and use
a bit to denote the data buffer. This application is also one of the test case
of Piko/RT (cond_3). Table 2 shows the results of the four verifications. Note
that the Safety case uses only assert to verify race condition, which is more
efficient than other liveness cases. Because the previous one only checks the
specific variable at the point, however, the LTL checks the variables along
every $\omega$-runs (Figure 1b). Moreover, the meaning of depth and states in
Table 2 are that the former represents the longest depth of the $\omega$-run
and the later is the number of states that Spin had verified. The state is the
set of all global variables in the model, each statement in the model might
causes the migration from one state to another.

The most interesting point is that the usage of memory is extreme high, is it
really worth it to consume such effort to build the verifications? Remember we
had mentioned about AWAITS statement, it is the watershed separating the
atomic and concurrent executing. Between each AWAITS (or A_AWAITS) statement
is an interrupt point that allowed every non-blocked process to be executed in
different order. There are total 67 AWAITS (and A_AWAITS) statements in our
model, and this is not counting the repeated ones (the inline function of
PROMELA will be expended like macro in C language). For example, there are
nine scheduling points in the model (8 in SVC and 1 in PendSV) which means we
have to multiple nine times the number of interrupt points under the inline
function of scheduling point. It is hard for us to consider such amount of
scheduling points at the same time by code review or test cases, how can we
check a vulnerability at the depth of 50 million steps? However, with the help
of the Model Checking and the powerful machine, we can verify those properties
within sustainable time. All we have to do is to construct an elegant model
which can use less steps to represent the real-world system.

Table 2. The 4 verification results | Depth | States | Memory | Time
---|---|---|---|---
Safety | 23,619,898 | 5.84e+09 | 314 GB | 3.2 hours
consu_starv | 49,295,820 | 1.01e+10 | 707 GB | 10.4 hours
produ_starv | 49,678,300 | 1.01e+10 | 707 GB | 10.4 hours
Deadlock | 40,484,755 | 8.11e+09 | 477.2 GB | 6.75 hours

Moreover, Spin also provides us an unreached statement list to analyze. The
followings reasons are certain for the unreached statements. Note that both
priority runqueues are not empty at the scheduling points (never switch to
idle thread) in this paper.

  * •

The scheduling point in PendSV needs to insert current task to the expired
runqueue, while the scheduling point in SVC don’t. This causes the unreached
statements.

  * •

If the active runqueue always has some elements, the scheduler does not need
to perform swap statements and the condition of next thread equals idle will
not be checked. This is because there is an enqueue point just before the
scheduling point.

  * •

If the active runqueue is empty and the expired runqueue has some elements,
the condition of next thread equals idle will not be checked.

  * •

If the next task is equal to the current task, need not to perform context
switch. This happens only in the pthread yield system call.

  * •

Two scheduling points in mutex unlock system call never been executed.

The last reason is complicated that we need to consider two conditions about
the mutex unlock system call. First is the system call from the condition of
LL/SC. The second is called via the condition wait system call. In the first
situation, consider that the current process has the lock, the thread state
must not be BLOCKED. The first scheduling point in mutex unlock system call is
guarded by the thread state equals BLOCKED condition will never be executed
under first situation. However, the first scheduling point will always be
approached in the second situation. Because the conditional statement in mutex
unlock system call is deterministic while the second scheduling point in mutex
unlock system call will never be executed. Those are the reason why there are
two scheduling point not be executed.

##  6\. Conclusions

We adapt an existing machine-assisted framework to fit the requirement of
model checking and verify several properties of a simple concurrent program
under the specific conditions. The model contains the simulation of hardware
and software aspects. Moreover, we do not construct any mathematical proof,
the PROMELA language is C-like that anyone can rebuild at any stages of the
system life cycle by their own (the effort of this paper is about 7 man-months
and the Piko/RT is still in development) and the verification time is within
one day (3 hours for safety property). This means model checking have its
advantage on verifying a real-world system at the early stage comparing to the
system optimized for formal verification.

However, there are still some defects in this paper that need to be
accomplished.

  1. (1)

The cost (time and memory usage) of adding one process to verify is too
expensive in checking the OS source code. There are two possible ways to deal
with. First, split the model into several layers and verify each layer one by
one. Another way is to construct proof by hand, Delzanno et al. (Delzanno et
al., 2014) has proved that using a limited number of process can represent the
situation of n processes in Spin.

  2. (2)

How to claim the abstract model and the real-world system are truly
homogeneous. One possible way is to construct a mechanism that extract the
PROMELA model from the C source code automatically rather than builds by
human.

For the second point, we can not claim the model in this paper is totally
correct, yet. But we can tell the behave is similar to the target system by
adding assert, analyzing the unreached statements or error message, and
applying the test cases. In this paper, we use condition variable to deal with
the mutual exclusion problem. We also adapted a mutex test case before, and
currently, we are trying to deal with the idle thread problem to look inside
the behavior of the model.

## References

  * (1)
  * Andronick et al. (2016) June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, and Christine Rizkallah. 2016\.  Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. In _Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings_. 52–68.  https://doi.org/10.1007/978-3-319-43144-4_4
  * ARM Limited (2014) ARM Limited 2014.  _ARMv7-M Architecture Reference Manual_.  ARM Limited.  https://developer.arm.com/docs/ddi0403/e/armv7-m-architecture-reference-manual.
  * Ben-Ari (2008) Mordechai Ben-Ari. 2008\.  _Principles of the Spin Model Checker_ (1 ed.).  Springer-Verlag London.
  * Blackham et al. (2011) B. Blackham, Y. Shi, S. Chattopadhyay, A. Roychoudhury, and G. Heiser. 2011.  Timing Analysis of a Protected Operating System Kernel. In _2011 IEEE 32nd Real-Time Systems Symposium_. 339–348.  https://doi.org/10.1109/RTSS.2011.38
  * Burr (2016) Phillip Burr. 2016\.  ARM CPU Solutions for IoT.  (Aug. 2016).  Retrieved April 12, 2018 from https://www.arm.com/files/pdf/20160830_03_ARM_CPU_Solutions_for_IoT_PhillipBurr.pdf Product Marketing Manager CPU Group, ARM.
  * Clarke (2008) Edmund M. Clarke. 2008\.  25 Years of Model Checking.  Springer-Verlag, Berlin, Heidelberg, Chapter The Birth of Model Checking, 1–26.  https://doi.org/10.1007/978-3-540-69850-0_1
  * Clarke et al. (1999) Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999\.  _Model Checking_.  MIT Press, Cambridge, MA, USA.
  * Delzanno et al. (2014) Giorgio Delzanno, Michele Tatarek, and Riccardo Traverso. 2014\.  Model Checking Paxos in Spin. In _Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, Verona, Italy, 10th - 12th September 2014_ _(Electronic Proceedings in Theoretical Computer Science)_ , Adriano Peron and Carla Piazza (Eds.), Vol. 161. Open Publishing Association, 131–146.  https://doi.org/10.4204/EPTCS.161.13
  * Holzmann (2003) Gerard J. Holzmann. 2003\.  _Spin Model Checker, the: Primer and Reference Manual_ (first ed.).  Addison-Wesley Professional.
  * Holzmann (2014) Gerard J. Holzmann. 2014\.  Mars Code.  _Commun. ACM_ 57, 2 (Feb. 2014), 64–73.  https://doi.org/10.1145/2560217.2560218
  * Holzmann (2018) Gerard J. Holzmann. 2018\.  Spin - Formal Verification.  (2018).  Retrieved April 11, 2018 from http://spinroot.com
  * Huang et al. (2018) Jim Huang, Yen-Kuan Wu, and Louie Lu. 2018.  pikoRT.  (2018).  Retrieved April 11, 2018 from https://github.com/PikoRT/pikoRT
  * Klein et al. (2009) Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009.  seL4: Formal Verification of an OS Kernel. In _Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles_ _(SOSP ’09)_. ACM, New York, NY, USA, 207–220.  https://doi.org/10.1145/1629575.1629596
  * Lamport (1977) Leslie Lamport. 1977\.  Proving the Correctness of Multiprocess Programs.  _IEEE Trans. Softw. Eng._ 3, 2 (March 1977), 125–143.  https://doi.org/10.1109/TSE.1977.229904
  * Lamport (1987) Leslie Lamport. 1987\.  A Fast Mutual Exclusion Algorithm.  _ACM Trans. Comput. Syst._ 5, 1 (Jan. 1987), 1–11.  https://doi.org/10.1145/7351.7352
  * Owicki and Gries (1976) Susan Owicki and David Gries. 1976.  An Axiomatic Proof Technique for Parallel Programs I.  _Acta Inf._ 6, 4 (Dec. 1976), 319–340.  https://doi.org/10.1007/BF00268134
  * Yiu (2013) Joseph Yiu. 2013\.  _The Definitive Guide to ARM Cortex-M3 and Cortex-M4 Processors_ (3rd ed.).  Newnes, Newton, MA, USA.
  * Zhang et al. (2015) Haitao Zhang, Toshiaki Aoki, and Yuki Chiba. 2015.  A Spin-Based Approach for Checking OSEK/VDX Applications. In _Formal Techniques for Safety-Critical Systems_ , Cyrille Artho and Peter Csaba Ölveczky (Eds.). Springer International Publishing, Cham, 239–255.