Safe Programming Methods

Lecturer: dr hab. inż. Paweł T. Wojciechowski, prof. PP

Web page in e-kursy: https://ekursy.put.poznan.pl/course/view.php?id=37629

Consultation: by e-mail

Over the past decades, Moore’s law has been in force: “the number of transistors in an integrated circuit doubles about every two years”. Each new generation of processors made the programs to work faster. However, this trend is changing. The future computer systems will have more and more CPU multi-core units, but each individual unit will not be faster than the unit from the previous year. Thus, to fully utilize the hardware capabilities, computations must be carried out concurrently.

Unfortunately, writing concurrent programs for contemporary computer architectures, which do not guarantee sequential consistency, is usually significantly more difficult than writing analogous sequential programs. In addition, testing such programs is difficult, and detecting and removing all programming errors in the code is not always possible.

The purpose of the lectures is to discuss some programming methods that allow you to write concurrent programs that are correct and efficient. Firstly, we will see how to use monitors correctly and efficiently. Next, we will discuss the alternative synchronization method, i.e. transaction memory. Secondly, we will present selected automatic verification methods. Thirdly, we will discuss some issues regarding the correctness of concurrent programs aimed for modern computer architectures. Finally, we will show example methods and languages that make it easy writing of parallel and distributed programs.

Below is a list of topics (Summer term 2024):

Safe concurrency (lectures)

Date	Synopsis, articles, and other materials	Slides
28.02	Discussion of the scope of the course and the form of assessment.
6.03	Repetition of selected material from the Concurrent and system programming course: Sections 1, 2, and 7 (only monitors).	slides
13.03, 20.03	Concurrent programming and synchronization on the example of monitors in C# or Java: basic monitor operations, correct access to shared data, invariants, correct design patterns, incorrect practices (e.g. double-check locking), deadlock, starvation, efficiency problems with lock conflicts and priority inversion, advanced synchronization problems and optimization (e.g., avoiding spurious wake-ups and spurious lock conflicts). An Introduction to Programming with C# Threads	slides
27.03	Detection of the race condition during program execution on the example of the Eraser tool: the lockset algorithm and its optimization (an initialization of variables, read-only shared data, read-write locks), correctness and completeness of the algorithm. Eraser: A Dynamic Data Race Detector for Multithreaded Programs	slides
3.04	Detection of the high-level data race condition by static analysis: the algorithm and its correctness and completeness (false positives – unnecessary warnings, false negatives – unnoticed errors). High-level Data Races	slides
10.04	Detection of programming errors (divide by zero, race condition, deadlock) based on model checking, on the example of the Java Pathfinder tool. Java Pathfinder (JPF)	slides
17.04	Conditional critical regions (CCR) and transactional memory: low-level operations on transactional memory, an implementation of CCR using these operations, data structures (ownership records and transaction descriptors), an algorithm of atomic writing to transactional memory. Language Support for Lightweight Transactions	slides
24.04	Correctness of concurrent access to shared objects: sequential and concurrent histories, the linearizability property, concurrent FIFO queue and register, linearizability properties (locality, blocking vs. non-blocking). Linearizability: A Correctness Condition for Concurrent Objects	slides
8.05, 15.05	Memory model on the example of Java language: a memory model as a specification of correct semantics of concurrent programs and legal implementations of compilers and virtual machines, weakness vs. strength of the memory model, contemporary limitations of the classical model of sequential consistency, global analysis and code optimization, the happens-before-based memory model and its weakness, the memory model taking into account circular causality, examples of controversial program code transformations. The Java Memory Model	slides
22.04	Parallel programming on the example of the Cilk language: programming constructs, the acyclic directed graph (DAG) as a model of multithreaded computing, performance measures on a multi-core processor, greedy scheduling and upper limits for computation time. A Minicourse on Multithreaded Programming Optional materials: OpenCilk: A Modular and Extensible Software Infrastructure for Fast Task-Parallel Code	slides
29.05	Distributed programming in the message-passing model on the example of the Erlang language (actors model, fault tolerance) and/or the Nomadic Pict language (process mobility, verification of the correctness of communication during compilation by static types).	slides
5.06	Distributed programming with guarantees of eventual consistency on the example of conflict-free replicated types (CRDTs) and cloud types. Cloud Types for Eventual Consistency Conflict-free Replicated Data Types A Comprehensive Study of Convergent and Commutative Replicated Data Types	slides
12.06	Colloquium

The OCaml language (labs)

There are two dominant paradigms in programming, functional and imperative. The goal of the lab. course is to provide an introduction to functional programming. Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids changing state and mutable data. During the course, we learn OCaml, a popular statically-typed functional programming language with an emphasis on expressiveness and safety.

Though languages and technologies change rapidly, many key ideas underlying the theory and practice of functional programming are immutable. The course will expose you to some of those ideas. The main topics raised during the course include:

1. Mathematical expressions and operators, comparison operators, boolean operators, programs as expressions.

2. Names, functions, basic types (int, float, string, char), type checking, type inference, type polymorphism (type variables).

3. Functions upon functions, anonymous functions (lambda expressions), partial function application (we apply only some of the arguments).

4. References (as an example of side effects).

5. Basic data types: lists, tuples, records.

6. Patterns and pattern matching.

7. List mapping, filtering, and folding.

8. Recursive functions, tail recursive functions (required in OCaml).

9. Exceptions and exception handlers.

10. Defining new types: constructors, polymorphism, recursive definitions.

11. Defining modules (sets of functions): abstraction, interfaces, functors.

12. Designing a library of polymorphic binary search trees (dictionaries).

13. Maps (dictionaries).

14. Mutable arrays.

15. Loops (while, for).

16. System programming: I/O operations, using files, graphics.

Example exercises:

1. Implement a function but-last, which takes a list l : 'a List as the only argument, and returns l without the last element. Try to implement this function in two variants: non-tail recursive and tail recursive. variants of this function.

2. Implement a function len which computes the number of elements in the list using fold_right i fold_left.

3. Implement a function reverse which reverses the order of the elements on the list.

4. Define a function append, which concatenates two lists, using a function List.fold_right.

5. Define two modules Inttree and Tree implementing binary trees, with values in leafs of type Int and of any type. The interfaces are specified here.

6. Create a module LMap from a standard module Map, which implements a map (dictionary) in which a key is a list of any type, and a value is of type Int. Two keys are identical if they have the same first element. Try all functions of the module LMap which were used for the standard module Map here.

The code snippets and solutions of the exercises: lab. 1, lab. 2, lab. 3, lab. 4, lab. 5. lab. 6. lab. 7. lab. 8.

Below are some useful links.

The OCaml home pages:

• OCaml.org:

  • Installing OCaml

  • Language Manual

  • Standard Library API

• v2.OCaml.org

On-line editors (good for learning):

• OCaml Playground

• Try OCaml

Here are some OCaml textbooks that you might find useful:

• OCaml from the Very Beginning (HTML | PDF)

  A very gentle introductory treatment of OCaml programming. Each small, self-contained chapter introduces a new topic in tutorial style.

• OCaml Programming: Correct + Efficient + Beautiful

  “A textbook on functional programming and data structures in OCaml, with an emphasis on semantics and software engineering. This book is the textbook for CS 3110 Data Structures and Functional Programming at Cornell University.”

• Introduction to Objective Caml

  “This book presents a practical introduction and guide to the language, with topics ranging from how to write a program to the concepts and conventions that affect how programs are developed in OCaml.”

• Real World OCaml - Functional Programming for the Masses

  “We wrote this book because we believe in the importance of programming languages, and that OCaml in particular is an important language to learn. Both of us have been using OCaml in our academic and professional lives for over 20 years, and in that time we’ve come to see it as a powerful tool for building complex software systems.”

• Developing Applications with Objective Caml (in PDF)

  A comprehensive, but a bit outdated, book on OCaml, covering not only the core language, but also modules, objects and classes, threads and systems programming, interoperability with C, and runtime tools.

• Unix system programming in OCaml (in PDF)

  This is an introductory course on Unix system programming, with an emphasis on communications between processes. The authors use OCaml instead of the C language that is customary in systems programming.

• Using, Understanding, and Unraveling the OCaml Language: From Practice to Theory and vice versa (in PDF)

  These course notes provide a formal description of the operational semantics (evaluation) and statics semantics (type checking) of core ML and of several extensions that appeared in OCaml (which originated from the ML language).

This document was generated on Apr 24, 2024.