VCManager HashMap nonlinearity

[hargoniX]

During a brief review of multi threaded data structure on the veil 2.0 branch I noticed that there is:

initialize vcManager : Std.Mutex (VCManager VCMetadata SmtResult) ← Std.Mutex.new (← VCManager.new vcManagerCh)

where VCManager is:

structure VCManager (VCMetaT ResultT: Type) where
  /-- All VCs, indexed by their ID. -/
  nodes : HashMap VCId (VerificationCondition VCMetaT ResultT)

  /-- Dependencies of each VC, i.e. VCs that must be proven before this
  VC can be proven. -/
  upstream : HashMap VCId (HashSet VCId)

  /-- In-degree count for each VC (number of upstream dependencies).
  Used for topological sorting: unfinished tasks with 0 in-degree
  should be executed next. -/
  inDegree : HashMap VCId Nat

  /-- Dependents of each VC, i.e. VCs that depend on _this_ VC. Used to
  update in-degrees when a task completes. -/
  downstream : HashMap VCId (HashSet VCId)

  /-- Maps primary VC IDs to their alternative VCs (e.g., TR-style).
  Alternative VCs are triggered when the primary VC's dischargers all fail. -/
  alternativeVCs : HashMap VCId (Array VCId) := HashMap.emptyWithCapacity

  /-- VCs that should NOT be started automatically (waiting for trigger).
  Used for alternative VCs that only run when their primary VC fails. -/
  dormantVCs : HashSet VCId := HashSet.emptyWithCapacity
....

and presumably these hashmaps are written to frequently for each generated verification condition. Due to the well known issue surrounding Array based structures that are market as mt this is going to cause many non linearities in the VC manager.

[dranov]

Thanks for reporting this, @hargoniX.

I don't expect it to be too much of an issue now (the bottleneck is the actual processing of VCs), but it's worth keeping track of.

What is the recommended way to work around the Array multi-threaded issue, for reference?

[hargoniX]

In general "don't do it". There are several things one might do to circumvent the issue. One could rearchitect the system to be channel based, use persistent data structures or (in very particular situations) use an Array of IO.Ref like I did in the channel implementation.