Abstract
Java monitors as implemented in the java.util.concurrent. locks package provide no-priority nonblocking monitors. That is, threads signalled after blocking on a condition queue do not proceed immediately, but they have to wait until both the signalling thread and possibly some of the others which have requested the lock release it. This can be a source of errors (if threads that get in the middle leave the monitor in a state incompatible with the signalled thread re-entry) or inefficiency (if repeated evaluation of preconditions is used to ensure safe re-entry). A concise implementation of priority nonblocking monitors in Java is presented. Curiously, our monitors are implemented on top of the standard no-priority implementation. In order to verify the correctness of our solution, a formal transition model (that includes a formalisation of Java locks and conditions) has been defined and checked using Uppaal. This model has been adapted to PlusCal in order to obtain a formal proof in TLA independent of the number of threads.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Buhr, P.A., Fortier, M., Coffin, M.H.: Monitor classification. ACM Computing Surveys 27, 63–107 (1995)
Carro, M., Mariño, J., Herranz, Á., Moreno-Navarro, J.J.: Teaching How to Derive Correct Concurrent Programs from State-Based Specifications and Code Patterns. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 85–106. Springer, Heidelberg (2004)
Chiao, H.-T., Wu, C.-H., Yuan, S.-M.: A More Expressive Monitor for Concurrent Java Programming. In: Bode, A., Ludwig, T., Karl, W.C., Wismüller, R. (eds.) Euro-Par 2000. LNCS, vol. 1900, pp. 1053–1060. Springer, Heidelberg (2000)
Allen Emerson, E., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)
Hansen, P.B.: Java’s insecure parallelism. ACM SIGPLAN Notices 34, 38–45 (1999)
Herranz, Á., Mariño, J., Carro, M., Moreno Navarro, J.J.: Modeling Concurrent Systems with Shared Resources. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 102–116. Springer, Heidelberg (2009)
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)
Lamport, L.: Specifying Systems. AddisonWesley (2004)
Lamport, L.: The PlusCal Algorithm Language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009)
Norvell, T.S.: Better monitors for Java. Javaworld, (October 2007), http://www.javaworld.com/javaworld/jw-10-2007/jw-10-monitors.html
TLA+. The Way to Specify, http://www.tlaplus.net/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herranz, Á., Mariño, J. (2012). A Verified Implementation of Priority Monitors in Java. In: Beckert, B., Damiani, F., Gurov, D. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2011. Lecture Notes in Computer Science, vol 7421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31762-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-31762-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31761-3
Online ISBN: 978-3-642-31762-0
eBook Packages: Computer ScienceComputer Science (R0)