St. Clair College - Windsor/South Campus

Progress of Concurrent Objects

Hongjin, Liang, author.

Boston [Massachusetts] : Now Publishing Inc., 2020.

1 PDF (106 pages) : color illustrations.

Implementations of concurrent objects in programming languages should guarantee linearizability and a progress property. These progress properties describe conditions under which a method call is guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Even worse, none of the existing results applies to concurrent objects with partial methods. Progress of Concurrent Objects examines the progress properties of concurrent objects. It formulates each progress property in terms of contextual refinement so that, when verifying clients of the objects, concrete object implementations can be replaced with their abstractions with certainty, achieving modular verification. For concurrent objects with partial methods, two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF) are described. Finally, a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects is introduced. This tutorial is intended for use by researchers and students. It surveys the current state of the topic and introduces the reader to recent advances in a tutorial style that makes the topic accessible to newcomers to the field. Provided by publisher.

Available

Electronic EbookElectronic Ebook

1 copy available at St. Clair College - Windsor/South Campus

LC Call No:

TJ211.49 .R63 2020eb

Dewey Class No:

629.8/924019 23

Author:

Hongjin, Liang, author.

Title:

Progress of Concurrent Objects / Hongjin, Liang; Xinyu, Feng.

Physical:

1 PDF (106 pages) : color illustrations.

ContentType:

text rdacontent

MediaType:

electronic isbdmedia

CarrierType:

online resource rdacarrier

Series:

Foundations and trends in information systems, 2331-124X ; 4:2

BibliogrphyNote:

Includes bibliographical references (pages 88-106).

Summary:

Implementations of concurrent objects in programming languages should guarantee linearizability and a progress property. These progress properties describe conditions under which a method call is guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Even worse, none of the existing results applies to concurrent objects with partial methods. Progress of Concurrent Objects examines the progress properties of concurrent objects. It formulates each progress property in terms of contextual refinement so that, when verifying clients of the objects, concrete object implementations can be replaced with their abstractions with certainty, achieving modular verification. For concurrent objects with partial methods, two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF) are described. Finally, a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects is introduced. This tutorial is intended for use by researchers and students. It surveys the current state of the topic and introduces the reader to recent advances in a tutorial style that makes the topic accessible to newcomers to the field. Provided by publisher.

AE:PersName:

Zhang, Qiaoning, author.

AE:PersName:

You, Sangseok, author.

AE:PersName:

Kim, Sangmi, author.

AE:PersName:

Esterwood, Connor, author.

AE:PersName:

Alahmad, Rasha, author.

AE:CorpName:

Now Publications, publisher.

AE:CorpName:

IEEE Xplore (Online Service), distributor.

Field Ind Subfield Data
001 001     3860126
005 005     20201005142656.0
006 006     m eo d
007 007     cr bn||||m|||a
008 008     200520s2020 maua ob 000 0 eng d
020 ISBN   $a ISBN  978-1-68083-673-8
    $q   online
020 ISBN   $z Canceled/invalid ISBN  9781680836622
    $q   print
035 System Ctrl No   $a System control number  (CaBNVSL)mat09062468
035 System Ctrl No   $a System control number  (IEEE)9062468
035 System Ctrl No   $a System control number  3860105
040 Cataloging Src   $a Original cataloging agency  CaBNVSL
    $b Language of cataloging  eng
    $e Description conventions  rda
    $c Transcribing agency  CaBNVSL
    $d Modifying agency  CaBNVSL
050 LC Call No $a Classification number  TJ211.49
    $b Item number  .R63 2020eb
082 Dewey Class No 04  $a Classification number  629.8/924019
    $2 Edition number  23
100 ME:PersonalName 1   $a Personal name  Hongjin, Liang,
    $e Relator term  author.
245 Title 10  $a Title  Progress of Concurrent Objects /
    $c Statement of responsibility  Hongjin, Liang; Xinyu, Feng.
264 ProductnNotice $a Place of prod/dist/manuf.  Boston [Massachusetts] :
    $b Name of prod./pub./dist./man.  Now Publishing Inc.,
    $c Date of prod/dist/manuf/copyrt  2020.
264 ProductnNotice $a Place of prod/dist/manuf.  [Piscataqay, New Jersey] :
    $b Name of prod./pub./dist./man.  IEEE Xplore,
    $c Date of prod/dist/manuf/copyrt  2020
300 Physical Desc   $a Extent  1 PDF (106 pages) :
    $b Other physical details  color illustrations.
336 ContentType   $a Content type term  text
    $2 Source  rdacontent
337 MediaType   $a Media type term  electronic
    $2 Source  isbdmedia
338 CarrierType   $a Carrier type term  online resource
    $2 Source  rdacarrier
490 SeriesStatement 1   $a Series statement  Foundations and trends in information systems,
    $x ISSN  2331-124X ;
    $v Vol. no./sequential designatn  4:2
504 BibliogrphyNote   $a Bibliography, etc. note  Includes bibliographical references (pages 88-106).
505 505 0   $a 505  1. Introduction -- 2. Literature review -- 3. Thrust area. 1. Human personality and human€€“robot interaction -- 4. Thrust area 2. Robot personality and human€€“robot interaction -- 5. Thrust area 3. Robot and human personality similarities and differences -- 6. Thrust area 4. Factors impacting robot personality -- 7. Major findings and a way forward -- References.
506 506   $a 506  Restricted to subscribers or individual electronic text purchasers.
520 Summary   $a Summary, etc. note  Implementations of concurrent objects in programming languages should guarantee linearizability and a progress property. These progress properties describe conditions under which a method call is guaranteed to complete. However, they fail to describe how clients are affected, making it difficult to utilize them in layered and modular program verification. Even worse, none of the existing results applies to concurrent objects with partial methods. Progress of Concurrent Objects examines the progress properties of concurrent objects. It formulates each progress property in terms of contextual refinement so that, when verifying clients of the objects, concrete object implementations can be replaced with their abstractions with certainty, achieving modular verification. For concurrent objects with partial methods, two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF) are described. Finally, a rely-guarantee style program logic LiLi for verifying linearizability and progress together for concurrent objects is introduced. This tutorial is intended for use by researchers and students. It surveys the current state of the topic and introduces the reader to recent advances in a tutorial style that makes the topic accessible to newcomers to the field.
    $c   Provided by publisher.
538 538   $a 538  Mode of access: World Wide Web.
588 588   $a 588  Description based on PDF viewed May 20, 2020.
650 Subj. $a Topical heading  Human-robot interactions.
650 Subj. $a Topical heading  Robotics.
655 655 $a 655  Electronic books.
700 AE:PersName 1   $a Personal name  Zhang, Qiaoning,
    $e Relator  author.
700 AE:PersName 1   $a Personal name  You, Sangseok,
    $e Relator  author.
700 AE:PersName 1   $a Personal name  Kim, Sangmi,
    $e Relator  author.
700 AE:PersName 1   $a Personal name  Esterwood, Connor,
    $e Relator  author.
700 AE:PersName 1   $a Personal name  Alahmad, Rasha,
    $e Relator  author.
710 AE:CorpName 2   $a Corporate name  Now Publications,
    $e Relator term  publisher.
710 AE:CorpName 2   $a Corporate name  IEEE Xplore (Online Service),
    $e Relator term  distributor.
830 830 $a 830  Foundations and trends in information systems ;
    $v   4:2.
    $x   2331-124X.
852 Holdings   $a Location  221
    $h Classification part  ebook
    $p Barcode  910
    $9 Cost  $0.00
856 ElectronicLocat 40  $3 Materials specified  Abstract with links to resource
    $u Uniform Resource Identifier  https://ra.ocls.ca/ra/login.aspx?inst=stclair&url=https://ieeexplore-ieee-org.eztest.ocls.ca/document/9097104

Google Books Preview

preview