BibTeX Proceedings details

BibTex html text dump of PaperDB database.

PaperDB is GPL Software, see: http://paperdb.sourceforge.net.

@InProceedings{Michaelson13,
  title = "{C}osting by {C}onstruction",
  author= "Michaelson, Greg",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "1--2",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "Predicting the performance of sequential systems is hard
     and concurrency brings additional complexities of
     coordination and timing. However, current models of
     concurrency tend to be unitary and so conflate computation
     and coordination. In contrast, the Hume language is based
     on concurrent generalised finite state boxes linked by
     wires. Boxes are stateless with transitions driven by
     pattern matching to select actions in a full strength
     functional language. This explicit separation of
     coordination and computation greatly eases concurrent system
     modelling: classical inductive reasoning may be used
     to establish properties within boxes, while box coordination
     may be explored independently through the novel box
     calculus. This seminar gives an introduction to the Hume
     language, cost models for Hume, and the box calculus, and
     considers how they might be integrated in a system to
     support costing by construction, where the
     resource implications of design decisions are made manifest
     as a system evolves."
}
@InProceedings{Turner13,
  title = "{N}ational {HPC} {F}acilities at {EPCC}: {E}xploiting {M}assively {P}arallel {A}rchitectures for {S}cientific {S}imulation",
  author= "Turner, Andrew",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "3--4",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "This presentation gives an overview of the challenges
     facing scientific software developers in exploiting current
     and upcoming massively parallel HPC facilities. The
     different levels of parallelism available in the
     architectures will be discussed, together with their impact
     for software design and what the trend is for the future.
     The discussion will be illustrated with examples from the
     two national facilities currently hosted at EPCC: HECToR (a
     Cray XE6) and the DiRAC IBM BlueGene/Q."
}
@InProceedings{GibsonRobinsonGoldsmith13,
  title = "{T}he {M}eaning and {I}mplementation of {SKIP} in {CSP}",
  author= "Gibson-Robinson, Thomas and Goldsmith, Michael",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "5--20",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "The CSP model checker FDR has long supported Hoare's
     termination semantics for CSP, but has not supported the
     more theoretically complete construction of Roscoe's,
     largely due to the complexity of adding a second termination
     semantics. In this paper we provide a method of simulating
     Roscoe's termination semantics using the Hoare termination
     semantics and then prove the equivalence of the
     two different approaches. We also ensure that FDR can
     support the simulation reasonably efficiently."
}
@InProceedings{HowellsdInverno13a,
  title = "{S}uccessful {T}ermination in {T}imed {CSP}",
  author= "Howells, Paul and d'Inverno, Mark",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "21--38",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "In previous work the authors investigated the
     inconsistencies of how successful termination was modelled
     in Hoare, Brookes and Roscoe's original CSP. This led to
     the definition of a variant of CSP, called CSPt. CSPt
     presents a solution to these problems by means of adding
     a termination axiom to the original process axioms. In this
     paper we investigate how successful process termination is
     modelled in Reed and Roscoe's Timed CSP, which is the
     temporal version of Hoare's original untimed CSP. We
     discuss the issues that need to be considered when selecting
     termination axioms for Timed CSP, based on our
     experiences in defining CSPt. The outcome of this
     investigation and discussion is a collection of candidate
     successful termination axioms that could be added to the
     existing Timed CSP models, leading to an improved treatment
     of successful termination within the Timed CSP framework. We
     outline how these termination axioms would be added to the
     family of semantic models for Timed CSP. Finally, we
     outline what further work needs to be done once these new
     models for Timed CSP have been defined. For example, it
     would then be possible to define timed versions of the new
     more flexible parallel operators introduced in CSPt."
}
@InProceedings{ChalmersKerridge13,
  title = "{V}erifying the {CPA} {N}etworking {S}tack using {SPIN}/{P}romela",
  author= "Chalmers, Kevin and Kerridge, Jon",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "39--52",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "This paper presents a verification of the CPA Networking
     Stack, using the SPIN Model Checker. Our work shows that the
     system developed for general networking within CPA
     applications works under the conditions defined for it. The
     model itself focuses on ensuring deadlock freedom, and work
     still needs to be undertaken to verify expected behaviour
     of the architecture."
}
@InProceedings{Boode13,
  title = "{I}mproving the {P}erformance of {P}eriodic {R}eal-time {P}rocesses: a {G}raph {T}heoretical {A}pproach",
  author= "Boode, Antoon H. and Broersma, Hajo and Broenink, Jan F.",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "57--80",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "In this paper the performance gain obtained by combining
     parallel periodic real-time processes is elaborated. In
     certain single-core mono-processor configurations, for
     example embedded control systems in robotics comprising many
     short processes, process context switches may consume a
     considerable amount of the available processing power.
     For this reason it can be advantageous to combine processes,
     to reduce the number of context switches and thereby
     increase the performance of the application. As we consider
     robotic applications only, often consisting of processes
     with identical periods, release times and deadlines, we
     restrict these configurations to periodic
     real-time processes executing on a single-core
     mono-processor. By graph theoretical concepts and means, we
     provide necessary and sufficient conditions so that the
     number of context switches can be reduced by combining
     synchronising processes."
}
@InProceedings{Friborg13,
  title = "{S}caling {P}y{CSP}",
  author= "Friborg, Rune Møllegard and Bjørndalen, John Markus and Vinter, Brian",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "81--92",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "PyCSP is intended to help scientists develop correct,
     maintainable and portable code for emerging architectures.
     The library uses concepts from Communicating Sequential
     Processes, CSP, and is implemented in the Python programming
     language. This paper introduces a new
     channel implementation and new process types for PyCSP that
     are intended to simplify writing programs for clusters. The
     new processes and channels are investigated by running 3
     benchmarks on two separate clusters, using up to 512 CPU
     cores. The results show that PyCSP scales well, with close
     to linear scaling for some of the benchmarks."
}
@InProceedings{Alam13,
  title = "{S}ervice {O}riented {P}rogramming in {MPI}",
  author= "Alam, Sarwar and Kamal, Humaira and Wagner, Alan",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "93--112",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "In this paper we introduce a service oriented approach to
     the design of distributed data structures for MPI. Using
     this approach we present the design of an ordered
     linked-list structure. The implementation relies on
     Fine-Grain MPI (FG-MPI) and its support for
     exposing fine-grain concurrency. We describe the
     implementation of the service and show how to compose and
     map it onto a cluster. We experiment with the service to
     show how its behaviour can be adjusted to match
     the application and the machine."
}
@InProceedings{Bate13,
  title = "{S}calable {P}erformance for {S}cala {M}essage-{P}assing {C}oncurrency",
  author= "Bate, Andrew",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "113--132",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "This paper presents an embedded domain-specific language for
     building massively concurrent systems. In particular, we
     demonstrate how ultra-lightweight cooperatively-scheduled
     processes and message-passing concurrency can be provided
     for the Scala programming language on the Java Virtual
     Machine (JVM). We make use of a well-known
     continuation-passing style bytecode transformation in
     order to achieve performance that is several orders of
     magnitude higher than native JVM threads. Our library is
     capable of scaling to millions of processes and messages on
     a single virtual machine instance, and our runtime system
     will detect deadlock should it occur. Message-passing is
     over 100 times faster than Erlang, and context switching is
     1000 times faster than native Java threads. In benchmarks,
     the performance of our library is close to compiled code."
}
@InProceedings{PedersenSmith13,
  title = "{P}rocess{J}: {A} {P}ossible {F}uture of {P}rocess-{O}riented {D}esign",
  author= "Pedersen, Jan Bækgaard and Smith, Marc L.",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "133--156",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "We propose ProcessJ as a new, more contemporary programming
     language that supports process-oriented design, which raises
     the level of abstraction and lowers the barrier of entry for
     parallel and concurrent programming. ProcessJ promises
     verifiability (e.g., deadlock detection), based on Hoare's
     CSP model of concurrency, and existing model checkers like
     FDR. Process-oriented means processes compose, unlike
     thread-based or asynchronous message-passing models
     of concurrency; this means that programmers can
     incrementally define larger and larger concurrent processes
     without concern for undesirable nondeterminism or unexpected
     side effects. Processes at their lowest, most granular level
     are sequential programs; there are no global variables, so
     no race conditions, and the rules of parallel composition
     are functional in nature, not imperative, and based on
     the mathematically sound CSP process algebra. Collectively,
     these ideas raise the level of abstraction for concurrency;
     they were successful once before with the occam language and
     the Transputer. We believe their time has come again, and
     will not go away, in this new age of multi-core processors.
     Computers have finally caught up with CSP
     and process-oriented design. We believe that ProcessJ can be
     the programming language that provides a bridge from today's
     languages to tomorrow's concurrent programs. Learning or
     teaching the programming model and language will be greatly
     supported through the educational part of the proposed
     project, which includes course templates and an online
     teaching tool that integrates in-browser programming
     with teaching material. Our efforts are encouraged by the
     forthcoming 2013 IEEE and ACM curricula guidelines, which
     for the first time include concurrent programming as a core
     knowledge area at the undergraduate level."
}
@InProceedings{HowellsdInverno13b,
  title = "{S}pecifying and {A}nalysing {N}etworks of {P}rocesses in {CSP}t (or {I}n {S}earch of {A}ssociativity)",
  author= "Howells, Paul and d'Inverno, Mark",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "157--184",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "In proposing theories of how we should design and specify
     networks of processes it is necessary to show that the
     semantics of any language we use to write down the intended
     behaviours of a system has several qualities. First in that
     the meaning of what is written on the page reflects the
     intention of the designer; second that there are
     no unexpected behaviours that might arise in a specified
     system that are hidden from the unsuspecting specifier; and
     third that the intention for the design of the behaviour of
     a network of processes can be communicated clearly and
     intuitively to others. In order to achieve this we have
     developed a variant of CSP, called CSPt, designed to solve
     the problems of termination of parallel processes present in
     the original formulation of CSP. In CSPt we introduced three
     parallel operators, each with a different kind of
     termination semantics, which we call synchronous,
     asynchronous and race. These operators provide specifiers
     with an expressive and flexible tool kit to define
     the intended behaviour of a system in such a way that
     unexpected or unwanted behaviours are guaranteed not to take
     place. In this paper we extend out analysis of CSPt and
     introduce the notion of an alphabet diagram that illustrates
     the different categories of events that can arise in the
     parallel composition of processes. These alphabet diagrams
     are then used to analyse networks of three processes
     in parallel with the aim of identifying sufficient
     constraints to ensure associativity of their parallel
     composition. Having achieved this we then proceed to prove
     associativity laws for the three parallel operators of CSPt.
      Next, we illustrate how to design and construct a network
     of three processes that satisfy the associativity law,
     using the associativity theorem and alphabet diagrams.
     Finally, we outline how this could be achieved for more
     general networks of processes."
}
@InProceedings{GibsonRobinson13a,
  title = "{E}fficient {S}imulation of {CSP}-{L}ike {L}anguages",
  author= "Gibson-Robinson, Thomas",
  editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
  pages = "185--204",
  booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
  isbn= "978-0-9565409-7-3",
  year= "2013",
  month= "nov",
  abstract= "In ''On the Expressiveness of CSP'', Roscoe provides a
     construction that, given the operational semantics rules of
     a CSP-like language and a process in that language,
     constructs a strongly bisimilar CSP process. Unfortunately,
     the construction provided is difficult to use and the
     scripts produced cannot be compiled by the CSP
     model-checker, FDR. In this paper, we adapt Roscoe's
     simulation to make it produce a process that can be checked
     relatively efficiently by FDR. Further, we extend Roscoe's
     simulation in order to allow recursively defined processes
     to be simulated in FDR, which was not supported by
     the original simulation. We also describe the construction
     of a tool that can automatically construct the simulation,
     given the operational semantics of the language and a script
     to simulate, both in an easy-to-use format."
}
@InProceedings{Teig13a,
  title = "{S}elective {C}hoice ''{F}eathering'' with {XCHAN}s",