Fred's Home Page

About me
csh is bad
Help out
KRoC/Linux (old)
occam upgrades
occam tutorial
Projects (PhD)
Quick gdb
UNIX crashcourse
WG / WGBuilder

Project Ideas

[ preamble | failure handling | formal verification | concurrent graphics | concurrent OS ]


This page is a pool of various project suggestions, targetted largely at PhD level and very open-ended. These relate to my main research interests; you can get a better idea of all that on my university home-page. Some of these may or may not be the same as those on the research group's project page. If you're interested in postgraduate study (at UKC), further information (relating particularly to application/funding) can be found on the department's postgraduate study page. The home-page for the programming languages and systems research group and the concurrency research blog may be of interest.

Of course, you're very welcome to suggest your own research project (or modify an existing one). These ideas/suggestions could also be MSc (research) projects, with some suitable scaling/pruning. Feel free to mail me if you have any questions. The department has a postgrad research FAQ that may answer some.

Failure handling in concurrent systems

Software-based protection in many modern languages is done using a try-except-finally based exception handling mechanism, that more or less provides an alternative return path between procedures. For some, particularly concurrent and process-oriented languages, this approach is sufficient for handling sequential code, but is unsuited for handling failure in networks of concurrent and communicating processes.

Research in this area will investigate existing approaches towards failure handling in software systems, both practical and theoretical, concentrating on failure handling in concurrent systems. Open questions include: given a network of communicating parallel processes in which one component fails, how should the components with which it is communicating be dealt with? The results of research in this area will include new or modified theories about the operation of concurrent systems, language bindings for providing a concise programmer interface and run-time support for the implementation of these.

Practical formal verification of concurrent systems

Much of the concurrency research undertaken at the University of Kent relates to the process-oriented abstraction of layered networks of communicating parallel processes. In these systems, thousands to millions of individual concurrent processes communicate with each other in well-defined ways to provide an overall functionality. Benefits of this approach include the ability to scale across single chips, multicore processes and distributed systems, as well as compositional and scalable approach to building these systems. Unlike traditional sequential systems, networks of concurrent processes can deadlock or livelock, errors arising from incorrect communication between components.

Research in this area will investigate practical approaches for the formal verification of concurrent systems. Some work in this area has already been undertaken at Kent as part of the RMoX project. Specifically, the automatic generation of CSP models of process behaviour from occam-pi source code, models which can then be checked against specifications in model-checkers such as FDR2. However, this is only a start and there are several unanswered questions, such as how to handle the dynamic reconfiguration of process networks. Within the context of RMoX, additional concerns include verification of low-level code code, e.g. to ensure that device-drivers interact with hardware devices in the intended (specified) way. This research project will broadly investigate these issues.

Concurrent graphics infrastructures

The mechanisms that application programs and graphical user-interfaces use to communicate are typically sequential, and often have relatively high overheads. Although a variety of approaches have been developed to remove some of these overheads (e.g. memory-mapped frame-buffer regions, direct-to-card GL support) a lot of the basic I/O mechanisms remain slow. Furthermore, with an application that has a multitude of windows on the screen, a lot of time both in the GUI and the application are spent mapping between on-screen 'visibles' and the corresponding program objects.

This project will survey the different mechanisms used to provide windowing systems (e.g. Microsoft Windows, the X Window System, Fresco (Berlin) and the Plan9 Windowing System) and the graphical 'toolkits' that typically sit between the application and the windowing interface (e.g. WX-windows, GDK/GTK/GTK+, Swing/AWT, and many more). The project will then investigate how concurrency can be leveraged to an advantage throughout -- from application processes or objects, through a common interface toolkit down to the driving of hardware (often through a framebuffer). Development is expected to take place in the context of the RMoX operating-system using the occam-pi programming language. The focus, however, is on the concurrency abstractions and the benefits that these can yield.

Highly concurrent operating-system components

Work is currently underway building CSP-based operating-system components. Implementation aspects of this project range from concurrent components (device-drivers, file-systems) down to low-level hardware interaction (e.g. controlling memory protection). Our key aims for this system are safety (formal methods), security (guarding against programmer error), scalability and reliability.

There is ample research opportunity within this project, and much may be relevant to other research areas. For example: investigating concurrent user interfaces; concurrent file-system management; and the management of a distributed concurrent operating-system.

Last modified: 2009-10-19 10:47:20.000000000 +0100 by Fred Barnes [ds] [plain]
Page generated: Sun Apr 28 11:39:33 2013
Valid XHTML 1.0! Valid CSS!