(key, value) lookup algos in src/common/lib/libc/gen
Hello Kernel people, et. al.,
I've been researching range querying over multi-dimensional keys,
(mainly related to its application in searching for ("delta","epsilon")
tuple timestamp range queries over a database of timers, events.)
This led me to the current key,value pair lookup code in the NetBSD
source so far. Some of what I found seems fragmented, sometimes
specialised, partially documented, possibly in disrepair.
Although daunting, it seems to be a worthy task to consolidate and
document the bits that need some attention/love.
I'm including a set of sources that I have identified - I'm sure I've
left some out. If so, please point me at them.
Network route matching related (key would be IP/prefix address):
- src/sys/net/radix.[ch]
- src/sbin/routed/radix.c
- src/sys/net/npf/lpm.[ch]
string matching:
Focussed on parallelism:
- src/sys/sys/thmap.h
- src/sys/kern/subr_thmap.c
Generic:
N-way Trie:
- src/common/lib/libc/gen/ptree.c
Radix Tr[ie]e
- src/common/lib/libc/gen/radixtree.c
RB Tree:
- src/common/lib/libc/gen/rb.c
Radix Priority Search Tree:
- src/common/lib/libc/gen/rpst.c
I'd like to understand if anyone here has looked
organising/consolidating these, and updating them to the state of the
art anytime recently, and if anyone has suggestions for new additions.
I'd also appreciate pointers to design patterns around a generalised
interface for these, that wouldn't take away from them.
Many Thanks for any comments.
--
Math/(~cherry)
Re: tickless kernel - high level roadmap ideas
> On Wed, 10 Apr 2024 12:37:31 +, Ice Cream > said: >> I've been working a little bit on how to tackle tickless in the >> kernel. I'll be hoping to send some preliminary patches later this month >> or so - so this is mostly an email to co-ordinate with anyone else >> working or aiming to work on similar things. > Hi, I'm aiming to work on this project as well. >> One of the first things needed will be to discover and manage underlying >> hardware timers which can interrupt at arbitrary (and/or repetitive) >> timeouts. Therefore, one of the first things I'll be working on is how >> to abstract this management. Since we need to support a variety of >> platform/CPU/CPU-package configurations, this will be the part with a >> large number of cross platform dependencies. > Since you'll be working on this, I'll start with researching about the next > step, > that is, the callout variants using bintime and the usage of the new timer > API. Brilliant! Let's take the details offline, so that we don't spam the list. I'll email you separately. -- Math/(~cherry)
tickless kernel - high level roadmap ideas
Hello NetBSD, I've been working a little bit on how to tackle tickless in the kernel. I'll be hoping to send some preliminary patches later this month or so - so this is mostly an email to co-ordinate with anyone else working or aiming to work on similar things. The only discernable change from an API consumption perspective for the rest of the kernel would be the appearance of bintime(9) variants of callout(9). Functionally, when tickless is enabled finally, any APIs which depend on sleep/wakeup semantics will have finer than 1/hz granularity. I can't think of any other discernable consumer facing changes at this point - feel free to mention them. To implement tickless however, things under the hood will need to change quite a bit. One of the first things needed will be to discover and manage underlying hardware timers which can interrupt at arbitrary (and/or repetitive) timeouts. Therefore, one of the first things I'll be working on is how to abstract this management. Since we need to support a variety of platform/CPU/CPU-package configurations, this will be the part with a large number of cross platform dependencies. Once this API is in place, the callout variants using bintime, described above, will need to be enabled to use this timer API in order to provide sub 1/hz granularity. Finally, consumers such as sleep/wakeup providers (cv_timedwaitbt(9), kpause(9) etc) and a whole bunch of other functions which depend upwards on these and others will need to be enabled to use the new sub 1/hz callout APIs. >From my initial experiments, and discussions with core@ , it looks like all this can be done mostly without changing the current hardclock(9) semantics - those semantics can simply be converted to use the new timer management API described above. Finally, the system time model can be updated to use high-res timers - I won't go into detail here, because it's a bit premature to speculate what that might look like - there seem to be a bunch of dependencies, including into CSF(9), softint(9), heartbeat(9), and anything that polls for timestamp updates (eg: timecounter(9) ). Looking forward to your comments and thoughts. Best, -- Math/(~cherry)
Re: tickless GSoc queries.
Hello,
I'm responding to these queries together, as I they are both within the
GSoc context, and I just saw them in the archives now.
I assume you've read through Taylor's post here:
https://wiki.netbsd.org/projects/project/tickless/
Since he's listed as the mentor for this project, I'll leave it to him
to respond if at all, regarding admin and GSoc related issues.
I'll leave some technical comments based on my own investigation of the
technical aspects of this project.
See inline below:
> "SD" == SD Asif Hossein writes:
[...]
SD> General Idea: In this project I am expected to implement the
SD> Tickless timer (Most probably dynamic tick or completely
SD> tickless or both) using the High-Resolution timers.
Can you explain what you mean by "dynamic tick" and how that relates to
"completely tickless" ?
SD> I have to implement the High-resolution timer support for that,
SD> as NetBSD's High-Resolution timer is still in development as far
SD> as I know.
There is hardware that has "high resolution timer" on several platforms
with support. For eg: even on the humble PC architecture, you can in
theory make the i8254 timer chip interrupt at anything upto the NTSC
resolution (which is slightly above a MHz, iirc). That is less of a
problem in this project - the hardware aspects of this project will
probably be faced when you are ready to integrate the code and get it to
run on the various platforms we support - and there are various port
masters who can assist you with that.
SD> I also have to implement the architecture independent APIs to
SD> adopt the configuration, change all the functions that use the
SD> periodic timer, hardclock to use the tickless timer and make
SD> them provide service/schedule when needed finally converting all
SD> the software subsystems to tickless so that they avoid periodic
SD> work altogether; increasing power consumption of NetBSD.
This is the meat of the project. I'd encourage you to look at
src/sys/kern_clock.c:hardclock() - which is the callback that the
current system calls at frequency hz (which is normally 100Hz).
Have a look at the following manual pages:
hardclock(9)
hz(9)
timecounter(9)
csf(9)
callout(9)
You can access them by going to https://man.netbsd.org and entering the
keywords in the corresponding text boxes and looking them up (assuming
you don't have a NetBSD system handy).
One of the first things you'll need to do is to define the kernel's
understanding of time. Right now, this is in the form of "tick"s - ie;
the number of ticks that have elapsed, or should elapse after/before an
event of interest. A tick event is assumed to happen once every 1/hz
seconds, and the event corresponds to the function hardclock() being
called.
In order to go tickless, it would be best to change the unit of kernel
timekeeping from ticks, which are very low resolution, to begin with, to
a more absolute and fixed resolution such as bintime(9) - it is defined
in sys/time.h as so:
struct bintime {
time_t sec;
uint64_t frac;
};
As you can see, this is far more accurate than any physical timer device
is capable of (the fraction has a resolution of 1/2 ^ 64 of a second -
which is a *lot*) - so you'll also need to figure out a way to represent
how to approximate the resolution. This approximation is called
"epsilon" in the kernel (read the comments around kern/kern_condvar.c
where bintime(9) is used in cv(9) variants such as cv_timedwaitbt(...)
Not only does epsilon help to bring down our resolution of consideration
to what the hardware is realistically capable of, it also helps us to
understand how to "cluster" together two event requests which are
fractionally closer together.
The key problem here has to do with callout(9) being our workhorse for
scheduling future callbacks within the kernel.
If we end up scheduling two callout(9) callbacks back-to-back to handle
those events, we'll end up being very busy in the kernel, handling tiny
fractionally separated events. Instead, we can just pretend the events
happened together within a span of "epsilon", and then call the
callback functions, which can decide whether this is a problem for them
or not.
This leads us to Taylor's milestones:
1. "... We need another data structure that provides good performance
for high-resolution sleeps without hurting the performance of the
existing call wheel for existing applications."
The main question here is viewable from the point of view of deciding
when to schedule the next callback. In order to do this, we need to look
up the list of pending scheduled events, make the approximations such as
the above, and then decide what the *nearest* bintime timestamp that
makes sense to be interrupted, so that we can run the next callback
is. All this needs to happen very efficiently, and Taylor's comment is
that the current implementation is efficient for an epsilon of 1/hz, but
not when your epsilon value goes down to finer
Re: hardclock(9) could go.
>>>>> Martin Husemann writes:
> On Wed, Mar 20, 2024 at 05:32:10AM +0000, Mathew, Cherry G.* wrote:
>> I look forward to your comments and test results, if any.
> I think moving heartbeat() to a callout context voids it's
> purpose.
Thanks, Martin.
Please find attached an updated patch.
This moves everything, except heartbeat() and callout_hardclock() out of
hardclock().
I'm mainly interested in understanding how statclock() behaves wrt
perf stat collection. The scheduler seems to behave ok, in my testing,
but ymmv.
More testing and feedback will help, please!
Many Thanks,
--
Math/(~cherry)
diff -r 5949662bc15a sys/kern/kern_clock.c
--- a/sys/kern/kern_clock.c Wed Mar 20 09:23:29 2024 +
+++ b/sys/kern/kern_clock.c Wed Mar 20 10:31:03 2024 +
@@ -107,6 +107,9 @@
static int sysctl_kern_clockrate(SYSCTLFN_PROTO);
+static callout_t clocktick_coh_var, *clocktick_coh =
+ &clocktick_coh_var; /* Callout handle for clock tick */
+
/*
* Clock handling routines.
*
@@ -222,6 +225,52 @@
return atomic_load_relaxed(&hardclock_ticks);
}
+static void
+clocktick(void *clkfrm)
+{
+ struct lwp *l;
+ struct cpu_info *ci;
+
+ ci = curcpu();
+ l = ci->ci_onproc;
+
+ clockrnd_sample(&hardclockrnd);
+
+ if(clkfrm != NULL) {
+ struct clockframe *frame = clkfrm;
+
+ ptimer_tick(l, CLKF_USERMODE(frame));
+
+ /*
+ * If no separate statistics clock is available, run it from here.
+ */
+ if (stathz == 0)
+ statclock(frame);
+ } /* called from initclocks with NULL */
+
+ /*
+ * If no separate schedclock is provided, call it here
+ * at about 16 Hz.
+ */
+ if (schedhz == 0) {
+ if ((int)(--ci->ci_schedstate.spc_schedticks) <= 0) {
+ schedclock(l);
+ ci->ci_schedstate.spc_schedticks = hardscheddiv;
+ }
+ }
+
+ if ((--ci->ci_schedstate.spc_ticks) <= 0)
+ sched_tick(ci);
+
+ if (CPU_IS_PRIMARY(ci)) {
+ atomic_store_relaxed(&hardclock_ticks,
+ atomic_load_relaxed(&hardclock_ticks) + 1);
+ tc_ticktock();
+ }
+
+ callout_schedule(clocktick_coh, 1); /* Schedule next one */
+}
+
/*
* Initialize clock frequencies and start both clocks running.
*/
@@ -254,6 +303,9 @@
*/
intr_timecounter.tc_frequency = hz;
tc_init(&intr_timecounter);
+ callout_init(clocktick_coh, CALLOUT_MPSAFE);
+ callout_setfunc(clocktick_coh, clocktick, NULL);
+ callout_schedule(clocktick_coh, 1); /* Schedule first one */
/*
* Compute profhz and stathz, fix profhz if needed.
@@ -302,49 +354,16 @@
void
hardclock(struct clockframe *frame)
{
- struct lwp *l;
- struct cpu_info *ci;
-
- clockrnd_sample(&hardclockrnd);
-
- ci = curcpu();
- l = ci->ci_onproc;
-
- ptimer_tick(l, CLKF_USERMODE(frame));
-
- /*
- * If no separate statistics clock is available, run it from here.
- */
- if (stathz == 0)
- statclock(frame);
- /*
- * If no separate schedclock is provided, call it here
- * at about 16 Hz.
- */
- if (schedhz == 0) {
- if ((int)(--ci->ci_schedstate.spc_schedticks) <= 0) {
- schedclock(l);
- ci->ci_schedstate.spc_schedticks = hardscheddiv;
- }
- }
- if ((--ci->ci_schedstate.spc_ticks) <= 0)
- sched_tick(ci);
-
- if (CPU_IS_PRIMARY(ci)) {
- atomic_store_relaxed(&hardclock_ticks,
- atomic_load_relaxed(&hardclock_ticks) + 1);
- tc_ticktock();
- }
-
/*
* Make sure the CPUs and timecounter are making progress.
*/
heartbeat();
/*
- * Update real-time timeout queue.
+ * Update real-time timeout queue, but update the frame first.
*/
- callout_hardclock();
+ callout_setfunc(clocktick_coh, clocktick, frame);
+ callout_hardclock();
}
/*
hardclock(9) could go.
Hello,
I'm investigating how to make our kernel less reliant on hardclock(9)
being called at hz(9).
Please find attached a patch to reduce hardclock(9)'s responsibilities
wrt the rest of the system timekeeping.
The idea is that hardclock(9) will drive callout_hardclock() for now,
until we modify the latter to not expect a fixed "tick" rate (ie; hz) -
at which point we have the option of several callers - for eg: a
carefully crafted one-shot interrupt at a programmable timespan.
With this patch, I'd like to understand what it does to the system as-is
- so ideally as many configs as possible (different arch/ and MP/UP) as
well as virtualisation situations (eg: Xen).
I look forward to your comments and test results, if any.
Many Thanks,
--
Math/(~cherry)
diff -r 95278b51da8b sys/kern/kern_clock.c
--- a/sys/kern/kern_clock.c Tue Mar 19 10:53:00 2024 +
+++ b/sys/kern/kern_clock.c Wed Mar 20 05:24:07 2024 +
@@ -107,6 +107,9 @@
static int sysctl_kern_clockrate(SYSCTLFN_PROTO);
+static callout_t clocktick_coh_var, *clocktick_coh =
+ &clocktick_coh_var; /* Callout handle for clock tick */
+
/*
* Clock handling routines.
*
@@ -222,6 +225,42 @@
return atomic_load_relaxed(&hardclock_ticks);
}
+static void
+clocktick(void *coptr)
+{
+ struct lwp *l;
+ struct cpu_info *ci;
+
+ ci = curcpu();
+ l = ci->ci_onproc;
+
+ /*
+ * If no separate schedclock is provided, call it here
+ * at about 16 Hz.
+ */
+ if (schedhz == 0) {
+ if ((int)(--ci->ci_schedstate.spc_schedticks) <= 0) {
+ schedclock(l);
+ ci->ci_schedstate.spc_schedticks = hardscheddiv;
+ }
+ }
+ if ((--ci->ci_schedstate.spc_ticks) <= 0)
+ sched_tick(ci);
+
+ if (CPU_IS_PRIMARY(ci)) {
+ atomic_store_relaxed(&hardclock_ticks,
+ atomic_load_relaxed(&hardclock_ticks) + 1);
+ tc_ticktock();
+ }
+
+ /*
+ * Make sure the CPUs and timecounter are making progress.
+ */
+ heartbeat();
+
+ callout_schedule(clocktick_coh, 1); /* Schedule next one */
+}
+
/*
* Initialize clock frequencies and start both clocks running.
*/
@@ -254,6 +293,10 @@
*/
intr_timecounter.tc_frequency = hz;
tc_init(&intr_timecounter);
+ callout_init(clocktick_coh, CALLOUT_MPSAFE);
+ callout_setfunc(clocktick_coh, clocktick, curcpu());
+ callout_schedule(clocktick_coh, 1); /* Schedule first one */
+ callout_hardclock(); /* And kick it down the road */
/*
* Compute profhz and stathz, fix profhz if needed.
@@ -318,33 +361,9 @@
if (stathz == 0)
statclock(frame);
/*
- * If no separate schedclock is provided, call it here
- * at about 16 Hz.
- */
- if (schedhz == 0) {
- if ((int)(--ci->ci_schedstate.spc_schedticks) <= 0) {
- schedclock(l);
- ci->ci_schedstate.spc_schedticks = hardscheddiv;
- }
- }
- if ((--ci->ci_schedstate.spc_ticks) <= 0)
- sched_tick(ci);
-
- if (CPU_IS_PRIMARY(ci)) {
- atomic_store_relaxed(&hardclock_ticks,
- atomic_load_relaxed(&hardclock_ticks) + 1);
- tc_ticktock();
- }
-
- /*
- * Make sure the CPUs and timecounter are making progress.
- */
- heartbeat();
-
- /*
* Update real-time timeout queue.
*/
- callout_hardclock();
+ callout_hardclock();
}
/*
Re: Resecting "options UVM_HOTPLUG"
>>>>> Santhosh Raju writes: > On Fri, Dec 1, 2023 at 6:42 AM Mathew Cherry G. wrote: >> >> Hi, >> >> After some discussion with Jason, and re-reading the code and its >> current state in code, I've come to the conclusion that it's in >> the interest of brevity to remove everything in sys/kern/ and >> sys/uvm/ which implement the "dynamic" part of uvm_hotplug(9). >> >> The top two reasons for this in my mind are: >> >> 1) There are no current users of the uvm_hotplug(9) KPI - >> balloon(9) uses it, but the unplug is unstable (wasn't able to >> debug this) and is thus disabled by default. >> >> 2) In order to do unplug without a balloon(9) like mechanism (eg: >> on native), there's a lot more state management code needed >> within uvm(9) - to make sure that RAM segments being unplugged >> have no machine references (eg: pmap related, pointers from >> inactive page tables, TLB pointers, etc. etc. ) >> >> This is a lot of per-architecture work, and there doesn't seem to >> be much demand for this feature (at least I haven't seen any >> comment related to this as a usecase). >> > I agree with these points and if the "dynamic" part is not being > used. I am assuming we are not completely removing the > UVM_HOTPLUG option? That's right - the static code is required for normal functioning of uvm(9) >> I believe that the project has had three useful purposes: >> >> 1) Demonstrated NetBSD code discipline - such a core part of the >> kernel code was developed entirely in userspace prior to >> integration - and due to the cross-compilable toolchain - it was >> done on Windows by fox@! >> >> 2) The re-org forced better modularisation in the relevant >> uvm/uvm_*.[hc] - ensuring even cleaner interfaces. >> >> 3) Demonstrated how TDD can reduce the pain of software dev. See: >> https://www.netbsd.org/gallery/presentations/santhosh/2017_AsiaBSDCon/ABC2017-P8B-uvm_hotplug-paper.pdf >> >> >> If there's no specific objection to this I'll be working with >> Jason to help make this is as painless as possible. >> > I am happy to offer any assistance needed to remove the related > code if needed since I did work on the tests part of it. That would be great - in fact, this is probably a great opportunity to rig the tests (src/tests/sys/uvm/) into the build system. Many Thanks, -- MattC/(~cherry)
Resecting "options UVM_HOTPLUG"
Hi, After some discussion with Jason, and re-reading the code and its current state in code, I've come to the conclusion that it's in the interest of brevity to remove everything in sys/kern/ and sys/uvm/ which implement the "dynamic" part of uvm_hotplug(9). The top two reasons for this in my mind are: 1) There are no current users of the uvm_hotplug(9) KPI - balloon(9) uses it, but the unplug is unstable (wasn't able to debug this) and is thus disabled by default. 2) In order to do unplug without a balloon(9) like mechanism (eg: on native), there's a lot more state management code needed within uvm(9) - to make sure that RAM segments being unplugged have no machine references (eg: pmap related, pointers from inactive page tables, TLB pointers, etc. etc. ) This is a lot of per-architecture work, and there doesn't seem to be much demand for this feature (at least I haven't seen any comment related to this as a usecase). I believe that the project has had three useful purposes: 1) Demonstrated NetBSD code discipline - such a core part of the kernel code was developed entirely in userspace prior to integration - and due to the cross-compilable toolchain - it was done on Windows by fox@! 2) The re-org forced better modularisation in the relevant uvm/uvm_*.[hc] - ensuring even cleaner interfaces. 3) Demonstrated how TDD can reduce the pain of software dev. See: https://www.netbsd.org/gallery/presentations/santhosh/2017_AsiaBSDCon/ABC2017-P8B-uvm_hotplug-paper.pdf If there's no specific objection to this I'll be working with Jason to help make this is as painless as possible. Many Thanks! -- MattC/(~cherry)
ARC model specified in spinroot/promela
Hello hackers,
I'm writing to introduce a project I've been working on off-and-on for a
while now - verifying parts of kernel code using a formal specifier[1]
Please find attached a patch to try out a formal verification run of the
Adaptive Replacement Cache by Megido et.al. [2]
You can try it out by installing spin from your favourite package
manager, and then running "make" in the current directory - it just
needs the usual C toolchain, afaik.
I'm hoping that someone can help me complete the current run, as I don't
have the computing resources required to run the full model (about 16GB
RAM). Meanwhile I'll keep finding ways to reduce the statespace
required.
The idea here is that once verified, the model can be written up as C
code, and then re-exracted using the modex [3] tool
I have some unpublished work that demonstrates this using the md(4)
NetBSD driver, but I want to be able to do a clean-room implementation
first, in order to get a better sense of a developer methodology I'm
going to call "DDD" or "D3" (Design Driven Development).
Bricks and boquets welcome. (Please Cc: me, as I am not subscribed to
the ML)
[1] https://spinroot.com/spin/whatispin.html
[2]
https://www.usenix.org/legacy/events/fast03/tech/full_papers/megiddo/megiddo.pdf
Fig. 4
[3] http://spinroot.com/modex/MANUAL.html
Best,
--
~cherry
diff -urN arc.null/arc.drv arc/arc.drv
--- arc.null/arc.drv 1970-01-01 00:00:00.0 +
+++ arc/arc.drv 2023-09-02 05:31:42.0 +
@@ -0,0 +1,97 @@
+/* $NetBSD$ */
+
+/* Spin model driver for NetBSD arc(9) arc.c written by cherry */
+
+/* XXX: Move these into a set of library includes ? */
+/* XXX: Equivalence verification */
+/* Note: CAS implemented in an atomic {} block */
+#define mutex_enter(_mutex) \
+ atomic {\
+ (_mutex == 0) -> _mutex = 1; \
+ }
+
+#define mutex_exit(_mutex) \
+ atomic {\
+ assert(_mutex == 1); \
+ (_mutex == 1) -> _mutex = 0; \
+ }
+
+#define N_ITEMS 6 /* Number of cache items to test with */
+#define IID_INVAL N_ITEMS /* Valid item.iid must be < N_ITEMS */
+#define C 5 /* Cache size - use judiciously - adds to statespace */
+#define ITEM_REPS 6 /* Max repeat item requests */
+
+typedef arc_item {
+ byte iid;/* Unique identifier for item */
+ bool cached;
+};
+
+/* Note that we use the arc_item.iid as the member lookup handle to reduce state space */
+typedef arc_list {
+ chan item_list = [C + 1] of { byte }; /* A list of page items */
+};
+
+#define lengthof(_arc_list) len(_arc_list.item_list)
+#define memberof(_arc_list, _arc_item) _arc_list.item_list??[eval(_arc_item.iid)]
+#define addMRU(_arc_list, _arc_item) _arc_list.item_list!_arc_item.iid
+#define readLRU(_arc_list, _arc_item) _arc_list.item_list?<_arc_item.iid>
+#define delLRU(_arc_list) _arc_list.item_list?_
+#define delitem(_arc_list, _arc_item) _arc_list.item_list??eval(_arc_item.iid)
+#define refreshitemto(_src_arc_list, _dest_arc_list, _arc_item) \
+ d_step { \
+ delitem(_src_arc_list, _arc_item); \
+ addMRU(_dst_arc_list, _arc_item); \
+ }
+#define refreshitem(_arc_list, _arc_item) refreshitemto(_arc_list, _arc_list, _arc_item)
+
+#define cachefetch(_arc_item) _arc_item.cached = true
+#define cacheremove(_arc_item) _arc_item.cached = false
+
+#define min(a, b) ((a < b) -> a : b)
+#define max(a, b) ((a > b) -> a : b)
+
+/* Declare arc lists */
+arc_list B1, B2, T1, T2;
+
+#define init_arc_item(_arc_item, _iid, _cached) \
+ d_step { \
+ _arc_item.iid = _iid; \
+ _arc_item.cached = _cached; \
+ }
+
+hidden arc_item _x[N_ITEMS]; /* Input state is irrelevant from a verification PoV */
+hidden byte _x_iid = 0;
+hidden byte _item_rep = 0;
+
+/* Temp variable to hold LRU item */
+hidden arc_item LRUitem;
+
+/* Adaptation "delta" variables */
+hidden byte d1, d2;
+byte p = 0;
+
+bit sc_lock;
+
+/* Drive the procs */
+init {
+
+ atomic {
+_x_iid = 0;
+ do
+:: _x_iid < N_ITEMS ->
+ init_arc_item(_x[_x_iid], _x_iid, false);
+ _item_rep = 0;
+ do
+ :: _item_rep < (_x_iid % ITEM_REPS) ->
+ run p_arc(_x[_x_iid]);
+ _item_rep++;
+ :: _item_rep >= (_x_iid % ITEM_REPS) ->
+ break;
+ od
+ _x_iid++;
+ :: _x_iid >= N_ITEMS ->
+ break
+ od
+ }
+
+}
diff -urN arc.null/arc.inv arc/arc.inv
--- arc.null/arc.inv 1970-01-01 00:00:00.0 +
+++ arc/arc.inv 2023-09-02 05:31:42.0 +
@@ -0,0 +1,19 @@
+/* $NetBSD$ */
+
+/* These are Linear Temporal Logic invariants (and constraints)
+ * applied over the statespace created by the promela
+ * specification. Correctness is implied by Logical consistency.
+ */
+ltl
+{
+ /* Liveness - all thread finally end */
+ eventually always (_nr_pr == 1) &&
+ /* Might look obvious, but make this explicit */
+ always ((lengthof(T1) <= C) &&
+ (lengthof(B1) <= C) &&
+ (lengthof(T2) <= C) &&
+ (lengthof(B2) <= C) ) &&
+ /* Not strictly true, but this forces a good dri
Re: [uvm_hotplug] Fixing the build of tests
On December 15, 2018 10:59:19 AM GMT+05:30, Santhosh Raju wrote: >Hello > >I noticed that the tests for uvm_hotplug(9) situated under >tests/sys/uvm/t_uvm_physseg.c was failing build. > >The reason for failure was the comparison between psize_t (which is >defined as unsigned log inside t_uvm_hotplug.c) and int resulting in a >sign compare error (-Werror=sign-compare). This was used to compare >the "npages" variable inside uvmexp struct. > >I have fixed the build by doing a type cast of uvmexp.npages to >psize_t and the changes have been attached as diff along with this >mail. The rationale for this is that uvmexp.npages is not expected to >go below zero and hence the type cast does not result in negative >values being converted to unsigned long. > >Cherry and I initially worked on this part of the code. And I would >like the tests to be able to build again, so that I can further probe >why some tests are failing. > >The test is currently not hooked into the build system, so this does >not cause build failures when building the kernel. > >Let me know if the patch looks good to commit. > >Regards >Santhosh Hi Santhosh, I believe the right thing to do would be to just fix the type in uvmexp.npages to the correct type instead of adjusting the test to accommodate it. What would be the consequences of this? Also, I hadn't realised that the tests aren't wired into the build. They really should be. Thanks! -- Sent from my Android device with K-9 Mail. Please excuse my brevity.
Re: Time accounting on statclock()
After fighting with this for a couple of weeks I realise there's a race that hits on faster machines. I'm trying to work backwards now - using the sched/queue mechanism on spllower on the current implementation to understand the timing issues better. It's been an intense week+ with little to show, but I've learned a lot. Ideally I would have wanted to model this using a formal specification, but since time is of importance I'm going to use the more straightforward method. I'll report back once I have something working. many thanks, Cherry -- Sent from my Android device with K-9 Mail. Please excuse my brevity.
