Cubicle

• Overview
• Download
  • Sources
  • Binaries
  • Installation instructions
• Publications
• Experiments
• Manual
  • Description language
  • Options
• Examples
• Contact

Flash

Cubicle model

Safety properties

Below are the safety properties we want to verify, in negated form.
Control properties:
∃ p. ( CacheState_home = CACHE_E ∧ CacheState[p] = CACHE_E )

∃ i,j. i≠j ∧ ( CacheState[i] = CACHE_E ∧ CacheState[j] = CACHE_E )

Data properties:
Dir_Dirty = False ∧ MemData ≠ CurrData

CacheState_home = CACHE_E ∧ CacheData_home ≠ CurrData
∃ p. ( CacheState[p] = CACHE_E ∧ CacheData[p] ≠ CurrData )

CacheState_home = CACHE_S ∧ Collecting = True ∧ CacheData_home ≠ PrevData
∃ p. ( CacheState[p] = CACHE_S ∧ Collecting = True ∧ CacheData[p] ≠ PrevData )

CacheState_home = CACHE_S ∧ Collecting = False ∧ CacheData_home ≠ CurrData
∃ p. ( CacheState[p] = CACHE_S ∧ Collecting = False ∧ CacheData[p] ≠ CurrData )

Options used

-brab 3 -forward-depth 14

Inferred invariants

All invariants are shown in their negated form, where #1 and #2 are distinct existentially quantified variables.

Home <> #1 &&
 Sort[#1] = Proc &&
 ProcCmd[#1] = NODE_Get &&
 UniMsg_Cmd[#1] = UNI_GetX

Dir_ShrVld = False &&
 Sort[#1] = Proc &&
 Dir_ShrSet[#1] = True

Home <> #1 &&
 Dir_ShrVld = False &&
 Sort[#1] = Proc &&
 Dir_ShrSet[#1] = True

CacheState_home <> CACHE_E &&
 Dir_Local = True &&
 Dir_Dirty = True

Dir_Pending = False &&
 Dir_Dirty = True &&
 CacheState[#1] = CACHE_S

CacheState_home = CACHE_S &&
 Dir_Pending = True

Dir_HeadVld = False &&
 CacheState[#1] = CACHE_S &&
 Dir_InvSet[#1] = False

UniMsg_Cmd_home = UNI_GetX &&
 Dir_Local = True

CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#1] = UNI_Get

Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#1] = UNI_GetX

UniMsg_Cmd_home = UNI_GetX &&
 CacheState[#1] = CACHE_S

Home <> #2 &&
 Dir_Pending = False &&
 Dir_ShrVld = False &&
 Sort[#1] = Proc &&
 Sort[#2] = Proc &&
 CacheState[#1] = CACHE_S &&
 CacheState[#2] = CACHE_S

Home <> #1 &&
 Sort[#1] = Proc &&
 ProcCmd[#1] = NODE_None &&
 InvMarked[#1] = True

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#1] = UNI_GetX

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#1] = UNI_Get

Home <> #1 &&
 Dir_Pending = False &&
 Dir_Dirty = True &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S

Home <> #1 &&
 Dir_Pending = False &&
 Dir_Dirty = True &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#1] = UNI_Nak

Home <> #1 &&
 UniMsg_Cmd_home = UNI_GetX &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S

Home <> #1 &&
 UniMsg_Cmd_home = UNI_GetX &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

ShWbMsg_Cmd = SHWB_FAck &&
 CacheState[#1] = CACHE_S

NakcMsg_Cmd = NAKC_Nakc &&
 CacheState[#1] = CACHE_S

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_FAck &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 NakcMsg_Cmd = NAKC_Nakc &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_Put &&
 RpMsg_Cmd[#1] = RP_Replace

Dir_Local = True &&
 ShWbMsg_Cmd = SHWB_FAck

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Put &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Dir_Local = True &&
 NakcMsg_Cmd = NAKC_Nakc

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_Nak

Home <> #2 &&
 Collecting = False &&
 Sort[#2] = Proc &&
 CacheState[#1] = CACHE_S &&
 UniMsg_Cmd[#2] = UNI_PutX

UniMsg_Cmd_home = UNI_PutX &&
 CacheState[#1] = CACHE_S

Dir_HeadVld = False &&
 Collecting = False &&
 CacheState[#1] = CACHE_S

Dir_Pending = True &&
 Dir_ShrVld = True

WbMsg_Cmd = WB_Wb &&
 CacheState[#1] = CACHE_S &&
 Dir_InvSet[#1] = False

CacheState_home = CACHE_E &&
 CacheState[#1] = CACHE_S &&
 Dir_InvSet[#1] = False

CacheState_home = CACHE_I &&
 Dir_Local = True &&
 Dir_Dirty = True

Home <> #1 &&
 UniMsg_Cmd_home = UNI_PutX &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 Dir_HeadVld = False &&
 Collecting = False &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 Dir_ShrVld = True &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Dir_Local = True &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

UniMsg_Cmd_home = UNI_Put &&
 Dir_Pending = False

UniMsg_Cmd_home = UNI_PutX &&
 Dir_Pending = False

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_Get

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_GetX

Home <> #1 &&
 Dir_ShrVld = True &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 Dir_HeadVld = False &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

CacheState_home = CACHE_S &&
 Dir_Local = False

Dir_ShrSet_home = True

CacheState_home = CACHE_S &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E

Collecting = False &&
 Sort[#2] = Proc &&
 CacheState[#1] = CACHE_S &&
 CacheState[#2] = CACHE_E

CacheState_home = CACHE_E &&
 Collecting = False &&
 CacheState[#1] = CACHE_S

Dir_Pending = True &&
 Dir_Dirty = False &&
 CacheState[#1] = CACHE_S &&
 Dir_InvSet[#1] = False

ProcCmd_home = NODE_Get &&
 Dir_Local = True

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 CacheState_home = CACHE_E &&
 Collecting = False &&
 Sort[#1] = Proc &&
 InvMarked[#1] = False &&
 UniMsg_Cmd[#1] = UNI_Put

CacheState_home = CACHE_E &&
 Dir_Dirty = False

UniMsg_Cmd_home = UNI_GetX &&
 Collecting = True

Home <> #1 &&
 Sort[#1] = Proc &&
 Dir_InvSet[#1] = False &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Dir_Local = True &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E

Home <> #1 &&
 Sort[#1] = Proc &&
 Dir_InvSet[#1] = False &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 Dir_HeadVld = False &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E

Dir_HeadVld = False &&
 ShWbMsg_Cmd = SHWB_ShWb

Dir_HeadVld = False &&
 Dir_ShrVld = True

UniMsg_Cmd_home = UNI_GetX &&
 ShWbMsg_Cmd = SHWB_FAck

UniMsg_Cmd_home = UNI_GetX &&
 ShWbMsg_Cmd = SHWB_ShWb

Dir_Dirty = True &&
 Dir_ShrVld = True

UniMsg_Cmd_home = UNI_GetX &&
 Dir_Pending = False

UniMsg_Cmd_home = UNI_GetX &&
 Dir_ShrVld = True

Home <> #1 &&
 UniMsg_Cmd_home = UNI_GetX &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_ShWb &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_FAck &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 UniMsg_Cmd_home = UNI_PutX &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Put &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 NakcMsg_Cmd = NAKC_Nakc &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 UniMsg_Cmd_home = UNI_GetX &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Sort[#1] = Proc &&
 ProcCmd[#1] <> NODE_Get &&
 UniMsg_Cmd[#1] = UNI_Get

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_ShWb &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_FAck &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

Home <> #1 &&
 Dir_Pending = False &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Put &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

Dir_Pending = False &&
 ShWbMsg_Cmd = SHWB_ShWb

CacheState_home = CACHE_E &&
 ShWbMsg_Cmd = SHWB_ShWb

UniMsg_Cmd_home = UNI_Put &&
 ShWbMsg_Cmd = SHWB_FAck

ShWbMsg_Cmd = SHWB_ShWb &&
 NakcMsg_Cmd = NAKC_Nakc

ShWbMsg_Cmd = SHWB_FAck &&
 NakcMsg_Cmd = NAKC_Nakc

UniMsg_Cmd_home = UNI_Put &&
 NakcMsg_Cmd = NAKC_Nakc

UniMsg_Cmd_home = UNI_PutX &&
 ShWbMsg_Cmd = SHWB_ShWb

Dir_Local = True &&
 ShWbMsg_Cmd = SHWB_ShWb

Dir_Dirty = False &&
 WbMsg_Cmd = WB_Wb

Dir_HeadVld = False &&
 WbMsg_Cmd = WB_Wb

Home <> #1 &&
 Sort[#1] = Proc &&
 ProcCmd[#1] <> NODE_Get &&
 UniMsg_Cmd[#1] = UNI_Put

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Get &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_Inv

Home <> #1 &&
 Dir_Pending = False &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

UniMsg_Cmd_home = UNI_Get &&
 ShWbMsg_Cmd = SHWB_ShWb

UniMsg_Cmd_home = UNI_Get &&
 ShWbMsg_Cmd = SHWB_FAck

UniMsg_Cmd_home = UNI_Put &&
 ShWbMsg_Cmd = SHWB_ShWb

CacheState_home = CACHE_E &&
 UniMsg_Cmd_home = UNI_Put

Dir_Dirty = False &&
 ShWbMsg_Cmd = SHWB_ShWb

Dir_Pending = False &&
 ShWbMsg_Cmd = SHWB_FAck

Dir_Pending = False &&
 NakcMsg_Cmd = NAKC_Nakc

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_PutX

UniMsg_Cmd_home = UNI_PutX &&
 Dir_Dirty = False

UniMsg_Cmd_home = UNI_PutX &&
 Dir_HeadVld = False

Home <> #1 &&
 ShWbMsg_Cmd = SHWB_ShWb &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Put &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

Home <> #1 &&
 UniMsg_Cmd_home = UNI_Get &&
 Sort[#1] = Proc &&
 InvMsg_Cmd[#1] = INV_InvAck

UniMsg_Cmd_home = UNI_Get &&
 Dir_Pending = False

UniMsg_Cmd_home = UNI_Put &&
 Dir_Dirty = False

ShWbMsg_Cmd = SHWB_ShWb &&
 Collecting = True

ShWbMsg_Cmd = SHWB_FAck &&
 Collecting = True

Home <> #1 &&
 Home <> #2 &&
 Sort[#1] = Proc &&
 Sort[#2] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX &&
 UniMsg_Cmd[#2] = UNI_PutX

CacheState_home = CACHE_E &&
 Dir_HeadVld = True

Home <> #1 &&
 UniMsg_Cmd_home = UNI_PutX &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

ShWbMsg_Cmd = SHWB_ShWb &&
 CacheState[#1] = CACHE_E

Home <> #1 &&
 Dir_Dirty = False &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

UniMsg_Cmd_home = UNI_Put &&
 CacheState[#1] = CACHE_E

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#1] = CACHE_S &&
 InvMsg_Cmd[#1] = INV_InvAck

Sort[#1] = Data &&
 CacheState[#1] = CACHE_S

UniMsg_Cmd_home = UNI_Get &&
 Collecting = True

UniMsg_Cmd_home = UNI_Put &&
 Collecting = True

Dir_Pending = False &&
 Collecting = True

ShWbMsg_Cmd = SHWB_ShWb &&
 ShWbMsg_Proc = Home

InvMarked_home = True

Home <> #1 &&
 Sort[#1] = Proc &&
 CacheState[#2] = CACHE_E &&
 UniMsg_Cmd[#1] = UNI_PutX

Home <> #1 &&
 CacheState_home = CACHE_E &&
 Sort[#1] = Proc &&
 UniMsg_Cmd[#1] = UNI_PutX

Dir_Dirty = False &&
 CacheState[#1] = CACHE_E

CacheState_home = CACHE_S &&
 Collecting = True
      

You can find the list of all invariants that can be extracted from BRAB here (also in negated form), this collection being inductive.

Search graph

The algorithm starts from the formula located at the bottom, inside a red octagon. Variables #1, #2, … that appear in the nodes are distinct skolem variables so we show a formula φ(#1, #2) as equivalent to ∃ z₁, z₂. z₁ ≠ z₂ ∧ φ(z₁, z₂). Plain black edges represent pre-image relations and are annotated by the transition instance that was considered. Black circles denote nodes that were obtained by pre-image computation and were not covered by already visited nodes. The nodes circled in gray are the one that were not useful because they were subsumed by formulas pointed by the gray dashed arrows. Approximations are shown in blue rectangles. Each approximation originates from the node that connects its rectangle with a bold dashed blue edge.

• Flash graph in dot format (33 MB)