Peter Welch's IFIP WG 2.4 Page
This page holds presentations made by Peter Welch at IFIP Working Group 2.4 (Software Implementation Technology).
Cape May (September, 2011)
Self-Verifying Concurrent Programming (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Jan B. Pedersen (UNLV), Frederick R.M. Barnes (Kent), Carl G. Ritson (Kent)
[Note: teaching material slides (13-37) have been added for completeness. They explore alternative synchronisation traces that are possible for the opening behaviour of Device (the running case study). Only slides 13 and 18-24 were presented on the day, because of time constraints. Such low-level exploration (slides 18-37) is for teaching purposes only: to check correct understanding of how the synchronisation primitives (channel communications and barriers) work. For engineering design and analysis, we should not need to consider behaviour at this level. The verify qualifiers and assertions shown later let us ask more useful questions (e.g. "does it deadlock or livelock?", "does it do things it shouldn't?", "does it do things it should?"), where the things (that it should or shouldn't do) are specified by the programmer-verifier writing ordinary (occam-π) program code.]
[Note: two "Postscript" slides have also been added.]
Self-Verifying Dining Philosophers (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Neil C.C. Brown (Kent)
[Related paper: Santa Claus: Formal Analysis of a Process-Oriented Solution, Peter H. Welch and Jan B. Pedersen. ACM Transactions on Programming Languages and Systems, 32(4):14:1-14:37, April 2010 (doi). Note: this paper predates and motivates the ideas presented in these two talks. It contains a short review of process-oriented design (section 2) and occam-π (section 3).]
[Conference: Communicating Process Architectures (CPA) 2012. The CPA series of conferences has been an important source of inspiration and support for most of the ideas documented here. CPA 2012 is the thirty fourth conference in this series and takes place at the University of Abertay, Scotland, from Sunday August 26th to Wednesday August 29th 2012. Paper submission deadline is 11 June 2012. Please consider attending, :).]
Fort Worden (May, 2009)
Multicore Scheduling for Lightweight Communicating Processes (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Carl G. Ritson (Kent), Adam T. Sampson (Abertay), Frederick R.M. Barnes (Kent), Peter H. Welch (Kent)
[Published: Multicore Scheduling for Lightweight Communicating Processes, Carl G. Ritson, Adam T. Sampson and Frederick R. M. Barnes. In Coordination Models and Languages, 11th International Conference, COORDINATION 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings, volume 5521 of Lecture Notes in Computer Science, pages 163-183. Springer, June 2009. Revised: Multicore Scheduling for Lightweight Communicating Processes in Science of Computer Programming, 77(6):727-740, Elsevier, May 2011.]
Engineering Emergence: an occam-π Adventure (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Kurt Wallnau (SEI, CMU), Adam T. Sampson (Abertay), Mark Klein (SEI, CMU)
[Published: To Boldly Go: an occam-π Mission to Engineer Emergence, Peter H. Welch, Kurt Wallnau, Adam T. Sampson, Mark Klein. In Natural Computing, DOI: 10.1007/s11047-012-9304-2, Springer, 2012.]
[Website: Complex Systems Modelling and Simulation Infrastructure (CoSMoS), Susan Stepney and Peter H. Welch and many others. CoSMoS was a joint project between the Universities of York and Kent, with supporting partners at Abertay and West of England. It ran from September 2007 through March 2012. Much of the work presented on this page had at least some (and often a crucial) role in the success of this project. The CoSMoS website has considerable content - see especially the demos.]
Lake Arrowhead (May, 2007)
A Process-Oriented Architecture for Complex System Modelling (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Carl G. Ritson (Kent)
[Published: A Process-Oriented Architecture for Complex System Modelling, Carl G. Ritson and Peter H. Welch. Concurrency and Computation: Practice and Experience, 22:965-980, Wiley, March 2010.]
[Related paper: Investigating Patterns for the Process-Oriented Modelling and Simulation of Space in Complex Systems, Adam T. Sampson, Peter H. Welch, Douglas N. Warren, Paul S. Andrews, John M. Bj�rndalen, Susan Stepney, and Jon Timmis. In Artificial Life XI: Proceedings of the Eleventh International Conference on the Simulation and Synthesis of Living Systems, pages 17-24, MIT Press, Cambridge, MA, USA, August 2008. ISBN 978-0-262-75017-2.]
[Course: Concurrency Design and Practice (occam-π version), Peter H. Welch. Note: following this Lake Arrowhead meeting, Kurt Wallnau invited and arranged for me to visit the Software Engineering Institute at CMU during October and November 2012, on sabbatical leave from my own university (Kent). This course was one of the deliverables for that visit. It is based upon an undergraduate course I teach at Kent, currently an elective module in the second year of the degree attracting around half the cohort (course numbers averaging just under 60 for academic years 2009-10, 2010-11 and 2011-12). I would rather this were a first year course, but I haven't been able to win that argument yet! The slides linked from the SEI/CMU course page will be maintained with the latest version of the course at Kent.]
Glasgow (July, 2006)
A Fast Resolution of Choice between Multiway Synchronisations (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent)
[Related paper: Alting Barriers: Synchronisation with Choice in Java using JCSP, Peter H. Welch, Neil C. C. Brown, James Moores, Kevin Chalmers, and Bernhard H. C. Sputh. In Concurrency and Computation: Practice and Experience, 22:1049-1062, Wiley, March 2010. Note: This paper reports how the technical material from the presentation has been integrated into the CSP for Java (JCSP) library, and explores a wider theme. See also Integrating and Extending JCSP (July 2007), referenced following the San Miniato presentation below. Further note: the July 2007 paper introduces several radical simplifications in the API for JCSP 1.1 (as well as new capabilities). The new API replaces and deprecates many prior mechanisms (e.g. for channel construction) that are used in the slides and papers on JCSP linked to below.]
[Related paper: Communicating Complex Systems, Peter H. Welch, Frederick R. M. Barnes and Fiona A.C. Polack. In Proceedings of the 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS-2006), pp. 107-117, Stanford, California, August 2006. IEEE ISBN: 0-7695-2530-X. Note: This paper has much of the technical material from the presentation, and explores one application and a wider theme.]
A CSP Model for Mobile Channels (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Frederick R. M. Barnes (Kent)
[Published: A CSP Model for Mobile Channels, Peter H. Welch and Frederick R. M. Barnes. In Communicating Process Architectures 2008, volume 66 of Concurrent Systems Engineering, pp. 17-33, September 2008. IOS Press, Amsterdam, the Netherlands. ISBN: 978-1-58603-907-3.]
Jackson's Mill (October, 2005)
Mobile Barriers: Semantics, Implementation and Application (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Frederick R. M. Barnes (Kent)
[Published: Mobile Barriers for occam-π: Semantics, Implementation and Application, Peter H. Welch and Frederick R. M. Barnes. In Communicating Process Architectures 2005, volume 63 of Concurrent Systems Engineering, pp. 289-316, September 2005. IOS Press, Amsterdam, the Netherlands. ISBN: 1-58603-561-4.]
[Note: the application on modelling blood clottting (restricted to a 1-D bloodstream) described in this presentation and paper was later developed into the 3-D version reported as part of the at Lake Arrowhead presentation (see above).]
Baden (January, 2005)
Freezing Mobile Processes: an Introduction to occam-π (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Frederick R. M. Barnes (Kent)
[Published: Communicating Mobile Processes: introducing occam-π, Peter H. Welch and Frederick R. M. Barnes. In Communicating Sequential Processes: the First 25 Years, Springer, Lecture Notes in Computer Science, April 2005, Volume 3525/2005, 712-713, DOI: 10.1007/11423348_10.]
[Related paper: Communicating Mobile Processes, Peter H. Welch and Frederick R. M. Barnes. In Communicating Process Architectures 2004, volume 62 of Concurrent Systems Engineering Series, pages 201-218, IOS Press (Amsterdam), The Netherlands, September 2004.]
[Note: the ideas for mobile processes presented at this Baden meeting substantially revise and extend the proposals made at Santa Cruz (see below), in part the result of feedback at the earlier meeting. It is these revised ideas that have been implemented in occam-π, with publications listed above. More recently, we have been considering bringing one of the ideas presented at Santa Cruz (multiple interfaces for mobile processes) back into occam-π, and making interface choice and usage secure through the notion of session types, checked by the compiler. Peter Welch, 14 May, 2012.]
[Related paper: Mobile Processes, Mobile Channels and Dynamic Systems, Eric Bonnici and Peter H. Welch. In 2009 IEEE Congress on Evolutionary Computation (CEC 2009), pages 232-239. IEEE Press, May 2009. ISBN 978-1-4244-2959-2. Note: this paper explores the duality between the concepts of mobile processes and mobile channels. It uses a dynamic complex system with emergent behaviours (ant foraging) as a case study and reports on the programming ease between the two approaches and the performance and speedup on multicore platforms. The case study uses the techniques presented at the Lake Arrowhead meeting (see above) and relies on the occam-π multicore scheduler reported at the Fort Worden meeting (also above).]
Santa Cruz (August, 2003)
Communicating Mobile Processes (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Frederick R. M. Barnes (Kent)
[Related paper: Prioritised Dynamic Communicating and Mobile Processes, Peter H. Welch and Frederick R. M. Barnes. In IEE Proceedings-Software, 150(2):121-136, April 2003. ISSN 1462-5970.]
[Note: see the note on the Baden presentation above.]
Dagstuhl (November, 2002)
Communicating Processes, Safety and Dynamics: the New occam (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Frederick R. M. Barnes (Kent)
[Related paper: Prioritised Dynamic Communicating Processes: Part 1, Frederick R. M. Barnes and Peter H. Welch. In Communicating Process Architectures 2002, volume 60 of Concurrent Systems Engineering, pages 321-352, IOS Press, Amsterdam, The Netherlands, September 2002. ISBN 1-58603-268-2.]
[Related paper: Prioritised Dynamic Communicating Processes: Part 2, Frederick R. M. Barnes and Peter H. Welch. In Communicating Process Architectures 2002, volume 60 of Concurrent Systems Engineering, pages 353-370, IOS Press, Amsterdam, The Netherlands, September 2002. ISBN 1-58603-268-2.]
Simon's Town (March, 2002)
CSP Networking for Java (JCSP.net) (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent), Jo Aldous (Kent), Jon Foster (Kent)
[Published: CSP Networking for Java (JCSP.net), Peter H. Welch, Jo Aldous and Jon Foster. In Computational Science - ICCS 2002, volume 2330 of Lecture Notes in Computer Science, pages 695-708. Springer-Verlag, April 2002. ISBN 3-540-43593-X.]
[Related paper: Cluster Computing and JCSP Networking, Peter H. Welch and Brian Vinter. In Communicating Process Architectures 2002, volume 60 of Concurrent Systems Engineering, pages 203-222, IOS Press, Amsterdam, The Netherlands, September 2002. ISBN 1 58603 268 2.]
San Miniato (May, 2001)
Communicating Processes, Components and Scaleable Systems (Abstract)
Slides: Powerpoint, PDF (1 per page) (6 per page)
Peter H. Welch (Kent)
[Note: this presentation raises some challenges to received wisdom on concurrency, components and complex systems. It argues for the use of concurrency as essential primitive for good software engineering (just as loops and functions are essential primitives), to be used every day without fear. Of course, it has to be the right kind of concurrency and the case for a model based on Hoare's CSP (Communicating Sequential Processes) is made. Reference is made to an extended occam multiprocessing language, the JCSP (CSP for Java) library and supporting results from formal verification of concurrency design patterns and implementations, but little detail is offered in the slides. Some of the relevant publications and websites are listed below.]
[Related paper: A Design Strategy for Deadlock-Free Concurrent Systems, Jeremy M. R. Martin and Peter H. Welch. In Transputer Communications, 3(4), John Wiley and Sons, June 1997. ISSN 1070-454X. Note: this builds a CSP model for client-server systems and formally verifies their freedom from deadlock and livelock, so long as no cycles of client-server relations are introduced. It also shows how client-server systems may be combined safely with I/O-PAR channel synchronisation, so that deadlock and livelock freedom is retained.]
[Related paper: A CSP Model for Java Multithreading, Peter H. Welch and Jeremy M. R. Martin. In Software Engineering for Parallel and Distributed Systems, pages 114-122. ICSE 2000, IEEE Computer Society Press, ISBN 0-7695-0634-8, June 2000. Note: this builds a CSP model of Java monitors (synchronized, wait, notify and notifyAll) and uses this to prove the correctness of the JCSP implementation of CSP channels. More generally, this CSP model enables the formal analysis of Java systems using these monitor mechanisms to check a range of important properties (such as the absence of deadlock).]
[Related paper: Formal Analysis of Concurrent Java Systems, Peter H. Welch and Jeremy M. R. Martin. In Communicating Process Architectures 2000, volume 58 of Concurrent Systems Engineering, pages 275-301, IOS Press (Amsterdam), ISBN 1 58603 077 9, September 2000. Note: this extends the work reported in the previous paper to verify the correctness of CSP choice (ALTing) in the JCSP implementation. This was prompted by the manifestation of a very obscure, very intermittent and fatal bug in this mechanism and the need to verify the fix. Applying the formal analysis to the original implementation showed up the bug immediately (which testing and use in the field had not discovered for over 2 years). There is an important lesson here.]
[Related paper: Integrating and Extending JCSP, Peter H. Welch, Neil C. C. Brown, James Moores, Kevin Chalmers, and Bernhard H. C. Sputh. In Communicating Process Architectures 2007, volume 65 of Concurrent Systems Engineering, pages 349-370, IOS Press (Amsterdam), ISBN 978-1586037673, July 2007. Note: this paper introduces several radical simplifications in the API for JCSP 1.1 (as well as new capabilities). The new API replaces and deprecates many prior mechanisms (e.g. for channel construction) that are used in the slides and papers on JCSP linked to above and below.]
[Website: JCSP Home Page]
[Tutorial: CSP for Java programmers (Pitfalls of multithreaded programming on the Java platform), Abhijit Belapurkar, IBM developerWorks, June 2005.]
[Tutorial: CSP for Java programmers (Concurrent programming with JCSP), Abhijit Belapurkar, IBM developerWorks, June 2005.]
[Tutorial: CSP for Java programmers (Advanced topics in JCSP), Abhijit Belapurkar, IBM developerWorks, June 2005.]
[Website: KRoC (occam-π) Home Page. See also occam-π: blending the best of CSP and the π-calculus.]
[Website: occam-π Quick Reference Wiki.]
[Course: Concurrency Design and Practice (occam-π version). See the note on this following the Lake Arrowhead meeting.]
[Conference: Communicating Process Architectures (CPA) 2012. See the note on this following the Cape May presentation above.]
[Website: WoTUG Home Page. WoTUG organises the CPA conferences and associated workshops and has been running since 1985. The website maintains a large amount of information/papers/software on concurrency and parallel computing, mostly (though not exclusively) themed around the ideas of communicating processes.]