This article presents the modelling of the ProcessJ cooperative runtime environment for the implementation of a CSP-inspired communication channel. We used the CSP tool FDR to verify the correctness of the ProcessJ runtime and primitives, demonstrating how we have overcome a limitation in the existing ProcessJ runtime to improve behaviour. However, our work has demonstrated a limitation when trying to claim a cooperatively-scheduled channel implementation meets the abstract specification of a CSP channel. Our conclusion is that without sufficient hardware to execute all processes at once, a channel implementation cannot fully meet its specification when considering the execution environment in which the channel must operate. We are assured that the ProcessJ channel works correctly, such as other implementations including JCSP and CSO, but we are not assured that modelling can use a pure CSP channel in place of a ProcesssJ channel or other implementation when undertaking modelling due to unintended prioritisation occurring when not enough resources are available for full concurrency. Our work has demonstrated the need to consider the execution environment as it may cause behavioural issues not detected when only modelling a system in the abstract.

In this article, we present the novel verification of synchronous channel communication and channel alternation (choice) by considering the environment within which our primitives are executing. Our work is in exploring development of a multi-threaded scheduler for a cooperatively scheduled process-oriented language, ProcessJ. We use communicating sequential processes to produce formal specifications for the implementation of the various parts of the language runtime (scheduler, runtime components, and generated code). We use established communicating sequential process specifications that model channel communication and choice as well as the formal verification tool FDR to formally prove that the implementations are correct and behave as expected, when executed by our scheduler (the execution environment). Our approach is novel and not seen in similar research, as we consider the behavior of the systems we examine under the restrictions imposed by an execution environment (a runtime system, a scheduler, an operating system, etc.) and show that even with such restrictions the channel communication and alternation work. More specifically, we show correctness when a system is executed by the ProcessJ cooperative scheduler. The main contributions of this work are in the models defined and method undertaken to verify cooperatively channel communication and choice.

There are many paradigms available to address the unique and complex problems introduced with parallel programming. These complexities have implications for computer science education as ubiquitous multi-core computers drive the need for programmers to understand parallelism. One major obstacle to student learning of parallel programming is that there is very little human factors evidence comparing the different techniques to one another, so there is no clear direction on which techniques should be taught and how. We performed a randomized controlled trial using 88 university-level computer science student participants performing three identical tasks to examine the question of whether or not there are measurable differences in programming performance between two paradigms for concurrent programming: threads compared to process-oriented programming based on Communicating Sequential Processes. We measured both time on task and programming accuracy using an automated token accuracy map (TAM) technique. Our results showed trade-offs between the paradigms using both metrics and the TAMs provided further insight about specific areas of difficulty in comprehension.

Abstract Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or reserved as anadvanceddiscipline for later study. Formal verification of system properties is often considered adifficultsubject area, requiring significant mathematical knowledge and generally restricted to smaller systems employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency and verification as a unified subject, as early as possible in the curriculum, so that they becomefundamentalelements of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency shouldsimplifythe expression of most scales and forms of computer system by reflecting the concurrency of the worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary mathematics into the concurrency models we use (CSP, π -calculus), the model checker (FDR) that lets us explore and verify those systems, and the programming languages/libraries (occam- π , Go, JCSP, ProcessJ) that let us design and build efficient executable systems within these models. This paper introduces a workflow methodology for the development and verification of concurrent systems; it also presents and reflects on two open-ended case studies, using this workflow, developed at the authors’ two universities. Concerns analysed include safety(don’t do bad things), liveness(do good things)and low probability deadlock(that testing fails to discover). The necessary technical background is given to make this paper self-contained and its work simple to reproduce and extend.

Lambda functions have become prevalent in mainstream programming languages, as they are increasingly introduced to widely used object oriented programming languages such as Java and C++. Some in the scientific literature argue that this feature increases programmer productivity, ease of reading, and makes parallel programming easier. Others are less convinced, citing concerns that the use of lambdas makes debugging harder. This thesis describes the design, execution and results of an experiment to test the impact of using lambda functions compared to the iterator design pattern for iteration tasks, as a first step in evaluating these claims. The approach is a randomized controlled trial, which focuses on the percentage of tasks completed, number of compiler errors, the percentage of time to fix such errors, and the amount of time it takes to complete programming tasks correctly. The overall goal is to investigate, if lambda functions have an impact on the ability of developers to complete tasks, or the amount of time taken to complete them. Additionally, it is tested if developers introduce more errors while using lambda functions and if fixing errors takes them more time. Lastly, the impact of experience level on productivity is evaluated by comparing the performance of participants from different levels of experience with one-another. Participants were assigned one of five levels based on their progress in the computer science major. The five levels were freshman, sophomore, junior, senior and professional. The professional level was assigned to individuals out of school with 5 or more years of professional experience. Results show that the impact of using lambdas, as opposed to iterators, on the number of tasks completed was significant. The impact on time to completion, number of errors introduced during the experiment and times spent fixing errors were also found to be significant. The analysis of the difference between the different levels of experience also shows a significant difference. The percentage of time spent on fixing compilation errors was 56.37% for the lambda group while it was 44.2% for the control group with 3.5% of the variance being explained by the group difference. 45.7% of the variance in the sample was explained by the difference between the level of education. Therefore, this study suggests that earlier findings that student results are comparable with the results of professional developers are to be considered carefully.

With the commercial development of multicore processors, the challenges of writing multithreaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware offers. Traditional approaches present concurrency as an advanced topic: they have proven difficult to use, reason about with confidence, and scale up to high levels of concurrency. This article reviews process-oriented design , based on Hoare's algebra of Communicating Sequential Processes (CSP), and proposes that this approach to concurrency leads to solutions that are manageable by novice programmers; that is, they are easy to design and maintain, that they are scalable for complexity, obviously correct , and relatively easy to verify using formal reasoning and/or model checkers. These solutions can be developed in conventional programming languages (through CSP libraries) or specialized ones (such as occam-π) in a manner that directly reflects their formal expression. Systems can be developed without needing specialist knowledge of the CSP formalism, since the supporting mathematics is burnt into the tools and languages supporting it. We illustrate these concepts with the Santa Claus problem , which has been used as a challenge for concurrency mechanisms since 1994. We consider this problem as an example control system, producing external signals reporting changes of internal state (that model the external world). We claim our occam-π solution is correct-by-design , but follow this up with formal verification (using the FDR model checker for CSP) that the system is free from deadlock and livelock, that the produced control signals obey crucial ordering constraints, and that the system has key liveness properties.