A History of BlockingQueues
This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1209.2239v1 |
| _version_ | 1819128485235392512 |
|---|---|
| author | Marina Zaharieva-Stojanovski Marieke Huisman Stefan Blom |
| author_facet | Marina Zaharieva-Stojanovski Marieke Huisman Stefan Blom |
| author_sort | Marina Zaharieva-Stojanovski |
| collection | DOAJ |
| description | This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures. |
| first_indexed | 2024-12-22T08:28:34Z |
| format | Article |
| id | doaj.art-5f4a863927584f5f9c303c76f9ee62f8 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-22T08:28:34Z |
| publishDate | 2012-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-5f4a863927584f5f9c303c76f9ee62f82022-12-21T18:32:34ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-09-0194Proc. FLACOS 2012313510.4204/EPTCS.94.4A History of BlockingQueuesMarina Zaharieva-StojanovskiMarieke HuismanStefan BlomThis paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.http://arxiv.org/pdf/1209.2239v1 |
| spellingShingle | Marina Zaharieva-Stojanovski Marieke Huisman Stefan Blom A History of BlockingQueues Electronic Proceedings in Theoretical Computer Science |
| title | A History of BlockingQueues |
| title_full | A History of BlockingQueues |
| title_fullStr | A History of BlockingQueues |
| title_full_unstemmed | A History of BlockingQueues |
| title_short | A History of BlockingQueues |
| title_sort | history of blockingqueues |
| url | http://arxiv.org/pdf/1209.2239v1 |
| work_keys_str_mv | AT marinazaharievastojanovski ahistoryofblockingqueues AT mariekehuisman ahistoryofblockingqueues AT stefanblom ahistoryofblockingqueues AT marinazaharievastojanovski historyofblockingqueues AT mariekehuisman historyofblockingqueues AT stefanblom historyofblockingqueues |