Kevin Elphinstone

Associate Professor

Dr Kevin Elphinstone is a Senior Lecturer with the School of Computer Science and Engineering. His research interests include:

  • Operating Systems
  • Microkernels
  • Multiserver Systems
  • Computer Architecture

publications

Conference Papers
add
Shen Y; Heiser G; Elphinstone K, 2019, 'Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs', in Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2019, pp. 188 - 200, http://dx.doi.org/10.1109/DSN.2019.00031
2019
Elphinstone K; Zarrabi A; McLeod K; Heiser G, 2017, 'A performance evaluation of rump kernels as a multi-server OS building block on seL4', in Proceedings of the 8th Asia-Pacific Workshop on Systems, APSys 2017, Mumbai, India, presented at APSys '17 Proceedings of the 8th Asia-Pacific Workshop on Systems, Mumbai, India, 02 September 2017 - 02 September 2017, http://dx.doi.org/10.1145/3124680.3124727
2017
Shen Y; Elphinstone K, 2015, 'Microkernel Mechanisms for Improving the Trustworthiness of Commodity Hardware', in European Dependable Computing Conference, IEEE, Paris France, pp. 155 - 166, presented at European Dependable Computing Conference, Paris France, 07 September 2015 - 11 September 2015, http://dx.doi.org/10.1109/EDCC.2015.16
2015
Peters S; Danis A; Elphinstone K; Heiser G, 2015, 'For a Microkernel, a Big Lock Is Fine', in APSys '15 Proceedings of the 6th Asia-Pacific Workshop on Systems, ACM, Tokyo, Japan, presented at ACM Asia-Pacific Workshop on Systems (APSys), Tokyo, Japan, 27 July 2015 - 28 July 2015, http://dx.doi.org/10.1145/2797022.2797042
2015
Elphinstone K; Heiser G, 2013, 'From L3 to seL4: What have we learnt in 20 years of L4 microkernels?', in SOSP 2013 - Proceedings of the 24th ACM Symposium on Operating Systems Principles, pp. 133 - 150, http://dx.doi.org/10.1145/2517349.2522720
2013
Andronick J; Greenaway D; Elphinstone KJ, 2010, 'Towards proving security in the presence of large untrusted components', in Proceedings of the 5th International Workshop on Systems Software Verification (SSV 2010), USENIX, online, presented at 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, BC, Canada, 06 October 2010 - 07 October 2010
2010
Heiser GA; Andronick J; Elphinstone KJ; Klein G; Kuz I; Ryzhyk L, 2010, 'The road to trustworthy systems', in Proceedings of the ACM Conference on Computer and Communications Security 2010, ACM, New York, pp. 3 - 9, Chicago, IL, 04 October 2010 - 08 October 2010, http://dx.doi.org/10.1145/1867635.1867638
2010
Klein G; Elphinstone K; Heiser G; Andronick J; Cock D; Derrin P; Elkaduwe D; Engelhardt K; Kolanski R; Norrish M; Sewell T; Tuch H; Winwood S, 2009, 'seL4: formal verification of an OS kernel', in Proceedings of SOSP`09, ACM, New York, NY, USA, pp. 207 - 220, presented at SOSP, Big Sky, Montana, USA, 11 October 2009 - 14 October 2009, http://dx.doi.org/10.1145/1629575.1629596
2009
Klein G; Derrin P; Elphinstone KJ, 2009, 'Experience report: seL4: formally verifying a high-performance microkernel', in Proceedings of the International Conference on Functional Programming, ACM, Edinburgh, Scotland, pp. 91 - 95, presented at ACM SIGPLAN Intl. Conf. on Functional Programming 2009, Edinburgh, Scotland, 31 August 2009 - 02 September 2009, http://dx.doi.org/10.1145/1596550.1596566
2009
Petters S; Lawitzky M; Heffernan R; Elphinstone KJ, 2009, 'Towards Real Multi-criticality Scheduling', in Proceedings of the 15th IEEE International Conference on embedded and Real-time Computing Systems and Application, IEEE Computer Society, Beijing, China, pp. 155 - 164, presented at 15th IEEE International Conference on Embedded and Real-time Computing Systems and Application, Beijing, China, 24 August 2009 - 26 August 2009, http://dx.doi.org/10.1109/RTCSA.2009.24
2009
Elkaduwe KW; Derrin PG; Elphinstone KJ, 2008, 'Kernel design for isolation and assurance of physical memory', in 1st workshop on isolation and integration in embedded systems, Glasgow, Scotland, pp. 35 - 40, presented at 1st workshop on isolation and integration in embedded systems, Glasgow, Scotland, 01 April 2008, http://dx.doi.org/10.1145/1435458.1435465
2008
Elkaduwe KW; Klein G; Elphinstone KJ, 2008, 'Verified protection model of the seL4 microkernel', in Proceedings of Verified Software: Theories, Tools and Experiments, 2008, Toronto, Canada, pp. 99 - 114, presented at Verified Software: Theories, Tools and Experiments (VSTTE) 2008, Toronto, Canada, 06 October 2008 - 09 October 2008, http://dx.doi.org/10.1007/978-3-540-87873-5-11
2008
Elphinstone KJ; Ruocco S; Greenaway D, 2007, 'Lazy queuing and direct process switch---merit of myths?', in National ICT Australia Technical Reports, OSPERT 2007 workshop on operating systems platforms for embedded real-time applications, Pisa, Italy, presented at OSPERT 2007 workshop on operating systems platforms for embedded real-time applications, Pisa, Italy, 03 June 2007
2007
Elphinstone KJ; Roscoe T; Heiser GA, 2007, 'Hype and Virtue', in 11th Workshop on Hot Topics in Operating Systems Proceedings - HotOS X1, 11th workshop on hot topics in operating systems proceedings - HotOS X1, San Diego, Californa, USA, presented at 11th workshop on hot topics in operating systems proceedings - HotOS X1, San Diego, Californa, USA, 07 May 2007 - 09 May 2007
2007
Elphinstone KJ; Klein G; Derrin PG; Roscoe T; Heiser GA, 2007, 'Towards a practical, verified kernel', in 11th Workshop on Hot Topics in Operating Systems Proceedings - HotOS X1, 11th workshop on hot topics in operating systems proceedings - HotOS X1, San Diego, Californa, USA, presented at 11th workshop on hot topics in operating systems proceedings - HotOS X1, San Diego, Californa, USA, 07 May 2007 - 09 May 2007
2007
Derrin PG; Elphinstone KJ; Elkaduwe D, 2007, 'A memory allocation model for an embedded microkernel', in National ICT Australia Technical Reports, 1st international workshop on microkernels for embedded systems MIKES 2007, Sydney, presented at 1st international workshop on microkernels for embedded systems MIKES 2007, Sydney, 16 January 2007
2007
Cock D; Elphinstone KJ; Klein G; Chakravarty MM; Derrin PG, 2006, 'Running the manual: an approach to high-assurance microkernel development', in 2006 ACM SIGPLAN Haskell workshop, Portland, Oregon, USA, pp. 60 - 71, presented at ACM SIGPLAN 2006 Haskell workshop, Portland, Oregon, USA, 17 September 2006
2006
Elphinstone KJ; Goetz S, 2004, 'Initial Evaluation of a User-level Device Driver Framework', in 9th Asia-Pacific Computer System Architecture Conference (ACSAC04), Beijing, China, pp. 256 - 269, presented at 9th Asia-Pacific Computer System Architecture Conference (ACSAC04), Beijing, China, 07 September 2004 - 09 September 2004
2004
Elphinstone KJ; Haeberlen A, 2003, 'User-Level Management of Kernel Memory', in 8th Asia-Pacific Conference, ACSAC 2003, Aizu-Wakamatsu, Japan, pp. 277 - 289, presented at 8th Asia-Pacific Conference, ACSAC 2003, Aizu-Wakamatsu, Japan, 23 September 2003 - 26 September 2003
2003
Aron M; Park Y; Jaeger T; Liedtke J; Elphinstone K; Deller L, 2001, 'The SawMill framework for virtual memory diversity', in Proceedings of the Australasian Computer Systems Architecture Conference, ACSAC, pp. 3 - 10, http://dx.doi.org/10.1109/ACAC.2001.903345
2001
Aron M; Park YJ; Jaeger T; Liedtke J; Elphinstone KJ; Deller L, 2001, 'The Saw Mill Framework of VM Density', in 6th Australasian Computer Systems Architecture Conference, 6th Australasian Computer Systems Architecture Conference, Gold Coast, Qld, presented at 6th Australasian Computer Systems Architecture Conference, Gold Coast, Qld, 29 January 2001 - 30 January 2001
2001
Geffaut A; Liedtke J; Tidswell JE; Jaeger T; Elphinstone KJ; Deller L; Park Y; Uhlig V; Reuther L, 2000, 'The SawMill multiserver approach', in Proceedings of the 9th Workshop on ACM SIGOPS European Workshop: Beyond the PC: New Challenges for the Operating System, EW 2000, pp. 109 - 114, http://dx.doi.org/10.1145/566726.566751
2000
Liedtke J; Völp M; Elphinstone K, 2000, 'Preliminary thoughts on memory-bus scheduling', in Proceedings of the 9th Workshop on ACM SIGOPS European Workshop: Beyond the PC: New Challenges for the Operating System, EW 2000, pp. 207 - 210, http://dx.doi.org/10.1145/566726.566768
2000
Jaeger T; Tidswell JE; Geaut A; Park Y; Elphinstone KJ; Liedtke J, 2000, 'Synchronous IPC over transparent monitors', in Proceedings of the 9th Workshop on ACM SIGOPS European Workshop: Beyond the PC: New Challenges for the Operating System, EW 2000, pp. 189 - 194, http://dx.doi.org/10.1145/566726.566765
2000
Jaeger T; Elphinstone K; Liedtke J; Panteleenko V; Park Y, 1999, 'Flexible access control using IPC redirection', in Proceedings of the Workshop on Hot Topics in Operating Systems - HOTOS, pp. 191 - 196
1999
Liedtke J; Uhlig V; Elphinstone K; Jaeger T; Park Y, 1999, 'How to schedule unlimited memory pinning of untrusted processes or provisional ideas about service-neutrality', in Proceedings of the Workshop on Hot Topics in Operating Systems - HOTOS, pp. 153 - 159
1999
Liedtke J; Elphinstone KJ; Schonberg S; Hartig H; Heiser GA; Islam N; Jaeger T, 1997, 'Achieved IPC Performance (Still the Foundation for Efficiency)', in 6th Workshop on Hot Topics in Operating Systems (HotOS), I E E E, COMPUTER SOC PRESS, Cape Cod, MA, USA, pp. 28 - 31, presented at 6th Workshop on Hot Topics in Operating Systems (HotOS), Cape Cod, MA, USA, http://dx.doi.org/10.1109/HOTOS.1997.595177
1997
Liedtke J; Elphinstone K; Schonberg S; Hartig H; Heiser G; Islam N; Jaeger T, 1997, 'Achieved IPC performance', in Proceedings of the Workshop on Hot Topics in Operating Systems - HOTOS, pp. 28 - 31
1997
Elphinstone KJ; Russell SM; Heiser GA; Liedtke J, 1997, 'Supporting Persistent Object Systems in a Single Address Space', in Connor R; Nettles S (ed.), 7th International Workshop on Persistent Object Systems, MORGAN KAUFMANN PUB INC, San Francisco, California USA, pp. 111 - 119, presented at 7th International Workshop on Persistent Object Systems, San Francisco, California USA, 29 May 1997 - 31 May 1997, http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:A1997BJ19K00010&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a
1997
Vochteloo J; Elphinstone KJ; Russell SJ; Heiser GA, 1996, 'Protection domain extensions in Mungi', in International Workshop on Object Orientation in Operating Systems 1996, Seattle, Washington, USA, pp. 161 - 165, presented at International Workshop on Object Orientation in Operating Systems 1996, Seattle, Washington, USA
1996
Russell S; Skea A; Elphinstone K; Heiser G; Burston K; Gorton I; Hellestrand G, 1992, 'Distribution + persistence = global virtual memory', in Proceedings - 2nd International Workshop on Object Orientation in Operating Systems, IWOOOS 1992, pp. 96 - 99, http://dx.doi.org/10.1109/IWOOOS.1992.252993
1992
Journal articles
add
Heiser G; Elphinstone K, 2016, 'L4 microkernels: The lessons from 20 years of research and deployment', ACM Transactions on Computer Systems, vol. 34, http://dx.doi.org/10.1145/2893177
2016
Elphinstone K; Zarrabi A; Danis A; Shen Y; Heiser G, 2016, 'An Evaluation of Coarse-Grained Locking for Multicore Microkernels', ArXiv, https://pdfs.semanticscholar.org/762a/284bd8b6ace609285f72f22dc1e03b004f33.pdf
2016
Klein G; Andronick J; Elphinstone K; Murray T; Sewell T; Kolanski R; Heiser G, 2014, 'Comprehensive Formal Verification of an OS Microkernel', ACM Transactions on Computer Systems, vol. 32, http://dx.doi.org/10.1145/2560537
2014
Elphinstone K; Shen Y, 2013, 'Increasing the trustworthiness of commodity hardware through software', Proceedings of the International Conference on Dependable Systems and Networks, http://dx.doi.org/10.1109/DSN.2013.6575328
2013
Klein G; Derrin P; Elphinstone K, 2009, 'Experience report: SeL4 :Formally verifying a high-performance microkernel', ACM SIGPLAN Notices, vol. 44, pp. 91 - 95
2009
Heiser GA; Elphinstone KJ; Kuz I; Klein G; Petters S, 2007, 'Towards trustworthy computing systems: taking microkernels to the next level', ACM Sigops Operating Systems Review, vol. 41, pp. 3 - 11, http://dx.doi.org/10.1145/1278901.1278904
2007
Leslie BJ; Chubb P; Fitzroy-Dale NJ; Gotz S; Gray CE; Macpherson LD; Potts DP; Elphinstone KJ; Heiser GA; Shen Y, 2005, 'User-level device drivers: Achieved performance', Journal of Computer Science and Technology, vol. 20, pp. 654 - 664, http://dx.doi.org/10.1007/s11390-005-0654-4
2005
Heiser GA; Elphinstone KJ; Vochteloo J; Russell SM; Liedtke J, 1998, 'The Mungi Single-Address-Space Operating System', Software-Practice and Experience, vol. 28, pp. 901 - 928, http://dx.doi.org/10.1002/(SICI)1097-024X(19980725)28:9<901::AID-SPE181>3.0.CO;2-7
1998
Liedtke J; Elphinstone K, 1996, 'Guarded page tables on mips R4600 or an exercise in architecture-dependent micro optimization', Operating Systems Review (ACM), vol. 30, pp. 4 - 15, http://dx.doi.org/10.1145/218646.218647
1996