Re: ARC model specified in spinroot/promela

Am 2023-09-14 16:40, schrieb Mathew, Cherry G.*:
> A few things remain WIP. Obviously, this is a "toy" model - it has 
> stack
> based "memory" management, and a directory buffer size of 64. So that
> needs to be hammered on a bit more. Further, I'm keen to now dip my 
> toes
> into re-entrancy. If you noticed in the earlier patches, there were
> model routines for "mutex_enter()/mutex_exit()". I'll re-look these and
> play around a little bit with concurrent entry of ARC() (ARC() is now
> strictly entered sequentially in a loop - see arc.drv). Once things
> settle down, I will look at making an actual block disk driver with an
> ARC(9) managed cache using this code.

Without having looked at anything in the code, and now with your comment 
about an "actual block disk driver"... AFAIR your ARC is based upon the 
paper, and this is not used anywhere in FreeBSD. ZFS is using a 
modified/adapted version of the ARC. What you are describing sounds a 
bit like our buffer cache 
(https://wiki.freebsd.org/BasicVfsConcepts#:~:text=Buffer%20cache%20is%20a%20layer,on%20a%20vnode%2Blbn%20basis.), 
but our buffer cache is not an ARC, it is AFAIR LRU eviction based.

I fully understand that you are far away from doing real modelling of 
such complex parts as the VFS parts of FreeBSD, but maybe this info 
gives a hint in terms of looking into some parts and see if you can 
adopt some parts in terms of design which can be anhanced later on to 
some real FreeBSD stuff...

Bye,
Alexander.

-- 
http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF
http://www.FreeBSD.org    netchild@FreeBSD.org  : PGP 0x8F31830F9F2772BF