vmware-labs / verified-betrfs

A verified high-performance file system
Other
31 stars 10 forks source link

rlimit fixes #1

Closed yizhou7 closed 3 years ago

yizhou7 commented 3 years ago

resolved some of the rlimit issues by using multiplier, the following is my local build result:

verification error:
  lib/DataStructures/LinearContentMutableMap.i.dfy
  BlockCacheSystem/JournalInterval.i.dfy
exceeded rlimit:
  ByteBlockCacheSystem/InterpretationDisk.i.dfy
  BlockCacheSystem/BlockJournalCache.i.dfy
  Impl/FlushPolicyModel.i.dfy
  Impl/IOImpl.i.dfy
  lib/Buckets/LKMBPKVOps.i.dfy
  Impl/GrowImpl.i.dfy
  PivotBetree/StatesViewPivotBetree_Refines_StatesViewMap.i.dfy
  Impl/SplitModel.i.dfy
  lib/Buckets/PackedKV.i.dfy
  Impl/SyncImpl.i.dfy
  Impl/MarshallingImpl.i.dfy
  Versions/CompositeView_Refines_TSJMap.i.dfy
  Betree/Graph.i.dfy
  Impl/EvictImpl.i.dfy
  Impl/DeallocImpl.i.dfy
  lib/Checksums/CRC32CArrayImpl.i.dfy
vmwclabot commented 3 years ago

@yizhou7, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.