{"entities":{"Q1085972":{"pageid":1096724,"ns":120,"title":"Item:Q1085972","lastrevid":66284250,"modified":"2026-04-12T08:46:43Z","type":"item","id":"Q1085972","labels":{"en":{"language":"en","value":"A generalized deadlock predicate"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3984555"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$BCD62A45-B468-4F68-9F00-06726393A892","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4ab3d39534487524644eff011d783c1ec286a601","datavalue":{"value":{"text":"A generalized deadlock predicate","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1085972$5772F4A2-1D1C-4D95-8722-ACAC130602D6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"723577c4817c3d3f719dabcb08f1deee3d3e6a3c","datavalue":{"value":"0608.68017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085972$A3672FEC-FC8A-4355-A051-B1BBF1B7A307","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b732bd03b87318943022211820a60624d65fe5f","datavalue":{"value":"10.1016/0020-0190(86)90133-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085972$39936C20-22FC-4F70-B100-1FE9BFD35070","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dcc379310c22a5a1105b18c81096ffc93d2801ba","datavalue":{"value":{"entity-type":"item","numeric-id":808174,"id":"Q808174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$BDC2E97A-1ECB-4D58-8263-39D78237C9FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"52c4b5b360bed7db2ba9926304f2212e9ab3bc0e","datavalue":{"value":{"entity-type":"item","numeric-id":1085971,"id":"Q1085971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$45B25AFF-4628-4105-8081-A171B41C5FC6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$14DAE69D-65E7-411A-9025-F39AF8461F04","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1085972$C1F52D6C-B769-4329-8589-901CFCD6C98A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"59d1dd8f2331a986d4a8cd2a907bc2058cfb3a57","datavalue":{"value":"Satisfiability of the deadlock predicate contructed by the semaphore invariant method is a necessary condition for total deadlock in PV programs. \\textit{E. M. Clarke jun.} [ACM Trans. Program. Lang. Syst. 2, 338-358 (1980; Zbl 0468.68024)] has developed a technique, based on a view of resource invariants as fixed points of a functional, for constructing a deadlock predicate such that satisfiability is a necessary and sufficient condition for total deadlock. We describe a technique for synthesizing a generalized deadlock predicate such that satisfiability is a necessary and sufficient condition for both total and partial deadlock. Our method constructs a strongest resource invariant using Clarke's fixed point functional. We then use this strongest resource invariant and a predicate transformer to construct a generalized deadlock predicate.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$B76AFA97-CE3F-404D-AC3E-63CDD0C0E3B8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085972$B3A5B1E7-B5C3-4387-AAFA-BEC01A3A7205","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"55662b70a63dadba6f87160c4efc08181f8bf858","datavalue":{"value":"3984555","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085972$2849C7D1-4553-4F98-8B5E-CDC2DFC77C44","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e278efc06f8225c382765bfa03cf3d084b8d9065","datavalue":{"value":"operating system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$B7A3DC25-F6C2-4AAC-8A39-DC678A8A988B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"db5e0888fa9957c443e210eb3c88f717e276ae13","datavalue":{"value":"parallel processing","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$4FB62508-3A61-413E-B65C-3C54C45EC15B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"171b65a7cb854c9ef61376c3217a3602a3fcb270","datavalue":{"value":"software reliability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$9B4DBACD-3A98-42E9-94F2-BC3FD6BEC815","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"29bd5141794a1bb885c47be97ee30e0627fa2608","datavalue":{"value":"semaphore invariant method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$9E6C97FC-F457-4DA0-B3AD-8108E32A9293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e58005d9b42d10d0c1b12b334a36de71ed443e4d","datavalue":{"value":"fixed point functional","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$E2B7C7CD-950E-4B0F-A0D7-EA9095FD9AA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"549d7add9d086a072dfebba0052fe0cde6454309","datavalue":{"value":"resource invariant","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$C177E57D-D008-449F-A276-1494319B8EA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f11205ddc68e722cd2520e50121e7f1457b1482","datavalue":{"value":"predicate transformer","type":"string"},"datatype":"string"},"type":"statement","id":"Q1085972$7D67A173-E8B7-4EAD-B41B-F3EEC480CBF7","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$6DE7F51E-DA72-481E-849C-5A72E5BA1C8D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"43f5ec35a87489328efbdd012ed15375a69a7975","datavalue":{"value":{"entity-type":"item","numeric-id":3922145,"id":"Q3922145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$D4D16BAB-F6FA-4B86-BC33-DD55C6B5C8FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"226149966044b48001c0682076573b6d91099455","datavalue":{"value":{"entity-type":"item","numeric-id":4773988,"id":"Q4773988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$912A8259-98AA-4E35-867D-33EB32A730BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5bc43b13fbf8e1626a092b7157a8555a9241847","datavalue":{"value":{"entity-type":"item","numeric-id":3914413,"id":"Q3914413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$F0A2BFF6-DFB6-428E-A7B8-292BE0191D30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42fda785ba06a1c78c3b1fa3da035e72d736ecb8","datavalue":{"value":{"entity-type":"item","numeric-id":4048566,"id":"Q4048566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$2F4E55CF-7A12-4E19-9F32-1388968BF3EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07eb19aa10f667730e5a63c1ac0122504f6e1ba1","datavalue":{"value":{"entity-type":"item","numeric-id":3862421,"id":"Q3862421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$030E93EE-06C0-4629-B874-5CE920606102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4672b026d99a8f6ea3a5edf58935ff86cbd1ad25","datavalue":{"value":{"entity-type":"item","numeric-id":1251066,"id":"Q1251066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$62CF7EF7-66AA-43F2-B011-1CE0DE3EB403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4a9238fc49995a79f8c006683b1a9c42fafe2bd","datavalue":{"value":{"entity-type":"item","numeric-id":4085221,"id":"Q4085221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1085972$8B903FE5-EAE7-4E0B-B805-0628A5FB3A6C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e0ad737fdabe499c9696ad970fdfc3d3d8aad187","datavalue":{"value":"https://doi.org/10.1016/0020-0190(86)90133-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q1085972$BFBFDC02-F403-42AD-8936-A726A46FD73F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cf2327bea31f7e0032fcd0451495362b3029c752","datavalue":{"value":"W2020682331","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1085972$75C01A8E-1585-4857-AD1C-FA983F12AF01","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1eeb509b73a042deebca797bb04c4d9ff9979f6f","datavalue":{"value":{"entity-type":"item","numeric-id":5711509,"id":"Q5711509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6f6f2c19e24b9eb7d5b78f60122585a02f92a56","datavalue":{"value":{"amount":"+0.759797215461731","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085972$7C444FF6-10D9-4581-AEBB-F5E132926829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f804cf18159ddb207bf79069e1cdbb9160b6a7c1","datavalue":{"value":{"entity-type":"item","numeric-id":580970,"id":"Q580970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1727a37e92d0897d508e5c7b1106c42128e27c7d","datavalue":{"value":{"amount":"+0.7456624507904053","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085972$4112D5BF-DCBA-4A15-AD0D-B9BB72617627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c587386bfa1332d76beca72089603ac21dae84f2","datavalue":{"value":{"entity-type":"item","numeric-id":2719638,"id":"Q2719638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bb5891abc879511a09d9756a15508efbd21d0c5","datavalue":{"value":{"amount":"+0.7422431111335754","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085972$5D610885-2D8F-447F-AE88-8B9A30D98CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"100f7a0d4450e2d738fe7d104e382306d825b2a3","datavalue":{"value":{"entity-type":"item","numeric-id":6108429,"id":"Q6108429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d47a3b1c4b54db1a2bebab30e6eddee55df37ac","datavalue":{"value":{"amount":"+0.7416718006134033","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085972$4BD8DBF2-E6A7-4F4B-ABAE-40A31FC33541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"add32c4af426ec3abfd90fc24a627e611654f481","datavalue":{"value":{"entity-type":"item","numeric-id":3608662,"id":"Q3608662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c73b379bf813c7abc117ae8d804229a3c96a9878","datavalue":{"value":{"amount":"+0.7326919436454773","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1085972$B90B9CA1-572D-4D3C-BD3B-7BFC078D8ECF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A generalized deadlock predicate","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_generalized_deadlock_predicate"}}}}}