model-checker.git
10 years agofix bug
Brian Demsky [Wed, 19 Sep 2012 07:25:45 +0000 (00:25 -0700)]
fix bug

10 years agoichange
Brian Demsky [Wed, 19 Sep 2012 00:15:01 +0000 (17:15 -0700)]
ichange

10 years agochanges
Brian Demsky [Tue, 18 Sep 2012 22:46:29 +0000 (15:46 -0700)]
changes

10 years agomore changes towards locks
Brian Demsky [Tue, 18 Sep 2012 08:15:06 +0000 (01:15 -0700)]
more changes towards locks

10 years agoMerge branch 'master' into mutex
Brian Demsky [Tue, 18 Sep 2012 05:18:56 +0000 (22:18 -0700)]
Merge branch 'master' into mutex

10 years agoadd mutex files
Brian Demsky [Tue, 18 Sep 2012 05:15:55 +0000 (22:15 -0700)]
add mutex files

10 years agoadd mutex files
Brian Demsky [Tue, 18 Sep 2012 05:15:55 +0000 (22:15 -0700)]
add mutex files

10 years agostart towards adding support for mutexes
Brian Demsky [Tue, 18 Sep 2012 05:15:35 +0000 (22:15 -0700)]
start towards adding support for mutexes

10 years agoMerge branch 'norris'
Brian Norris [Fri, 14 Sep 2012 18:25:59 +0000 (11:25 -0700)]
Merge branch 'norris'

10 years agomodel: release_seq synchronization generates mo_graph edge "work entries"
Brian Norris [Fri, 14 Sep 2012 18:07:22 +0000 (11:07 -0700)]
model: release_seq synchronization generates mo_graph edge "work entries"

Now, when the synchronization for a ModelAction is updated while resolving
release sequences, the affected ModelAction(s) can be queued to the work_queue
for later processing (i.e., checking for mo_graph edge additions).

Note that the MOEdgeWorkEntry is not yet handled in the work_queue loop.

10 years ago.gitignore: ignore .dot graph files
Brian Norris [Fri, 14 Sep 2012 17:33:53 +0000 (10:33 -0700)]
.gitignore: ignore .dot graph files

10 years agomodel: record the number of feasible executions
Brian Norris [Fri, 14 Sep 2012 17:24:24 +0000 (10:24 -0700)]
model: record the number of feasible executions

The 'num_executions' statistic isn't quite as useful now. We want to compare
total executions to the number of feasible executions.

10 years agoconfig: don't enable graph dumping in master repo
Brian Norris [Fri, 14 Sep 2012 17:29:35 +0000 (10:29 -0700)]
config: don't enable graph dumping in master repo

10 years agomodel: add work queue loop
Brian Norris [Fri, 14 Sep 2012 16:52:49 +0000 (09:52 -0700)]
model: add work queue loop

This commit does not change the actual computations performed yet. It only
prepares a loop structure in which we could perform many different Work items,
queueing them up as they are generated.

10 years agoworkqueue: add work queue structures
Brian Norris [Fri, 14 Sep 2012 16:46:56 +0000 (09:46 -0700)]
workqueue: add work queue structures

10 years agotabbing
Brian Demsky [Fri, 14 Sep 2012 08:33:48 +0000 (01:33 -0700)]
tabbing

10 years ago(1) add actions for the fence
Brian Demsky [Fri, 14 Sep 2012 08:31:09 +0000 (01:31 -0700)]
(1) add actions for the fence
(2) a little more support for cyclegraph -- show rmw edges
(3) add extra documentation for norris

10 years agoadd support for dumping cyclegraphs as dot files... also eliminate redundant edges...
Brian Demsky [Fri, 14 Sep 2012 05:04:45 +0000 (22:04 -0700)]
add support for dumping cyclegraphs as dot files...  also eliminate redundant edges to make them easier to view

10 years agomodel: more restructuring of read/write processing
Brian Norris [Thu, 13 Sep 2012 23:16:30 +0000 (16:16 -0700)]
model: more restructuring of read/write processing

Make a ModelChecker::process_write function, for symmetry and to shorten the
code portions where the main control flow happens.

10 years agomodel: remove unnecessary parameter to ModelChecker::process_read
Brian Norris [Thu, 13 Sep 2012 23:08:04 +0000 (16:08 -0700)]
model: remove unnecessary parameter to ModelChecker::process_read

The current Thread can be generated later.

10 years agoMakefile: add PHONY targets
Brian Norris [Thu, 13 Sep 2012 23:03:23 +0000 (16:03 -0700)]
Makefile: add PHONY targets

Just in case there ever are files named clean, mrclean, etc.

10 years agobugfix: straighten out STL vector allocation (snapshotted vs. persistent)
Brian Norris [Thu, 13 Sep 2012 22:42:21 +0000 (15:42 -0700)]
bugfix: straighten out STL vector allocation (snapshotted vs. persistent)

When using a STL data structure allocated on the stack, we must make sure its
elements are allocated with the same allocator as the structure. For instance,
in a model-checking context, the stack is persistent (non-snapshotting), so any
stack-allocated std::vector should use the non-snapshotting allocator (i.e.,
MyAlloc).

At the same time, clarify CycleGraph and CycleNode classes by labelling them as
SNAPSHOTALLOC.

10 years agomodel: bugfix - don't clobber 'updated'
Brian Norris [Thu, 13 Sep 2012 21:58:36 +0000 (14:58 -0700)]
model: bugfix - don't clobber 'updated'

The 'updated' variable should stay 'true' even if modification orders and
promises aren't updated by the "write" checks. This could be a RMW which made
updates via the "read" checks.

10 years agoRevert "Makefile: don't always rebuild make.deps"
Brian Norris [Thu, 13 Sep 2012 21:56:16 +0000 (14:56 -0700)]
Revert "Makefile: don't always rebuild make.deps"

The Makefile wasn't using its dependency generation correctly. Revert this for
now.

This reverts commit 870ba814eceb1afee4eefb17dab3980549ca73e2.

10 years agosnapshot: print stack trace on segfault
Brian Norris [Thu, 13 Sep 2012 21:47:44 +0000 (14:47 -0700)]
snapshot: print stack trace on segfault

10 years agocommon: add print_trace() for backtracing
Brian Norris [Thu, 13 Sep 2012 21:47:23 +0000 (14:47 -0700)]
common: add print_trace() for backtracing

10 years agomodel: trivial fixups
Brian Norris [Thu, 13 Sep 2012 18:45:42 +0000 (11:45 -0700)]
model: trivial fixups

10 years agoMakefile: don't always rebuild make.deps
Brian Norris [Thu, 13 Sep 2012 18:35:48 +0000 (11:35 -0700)]
Makefile: don't always rebuild make.deps

The dependencies don't need to be regenerated for "make tags", "make docs",
etc.

10 years agomodel: simple ASSERT() bug
Brian Norris [Thu, 13 Sep 2012 17:16:37 +0000 (10:16 -0700)]
model: simple ASSERT() bug

Don't ASSERT(rf->is_write()) until we're sure that rf is non-NULL.

10 years agomain: wrap help message
Brian Norris [Thu, 13 Sep 2012 17:04:28 +0000 (10:04 -0700)]
main: wrap help message

10 years agomodel: kill unneeded local variable
Brian Norris [Thu, 13 Sep 2012 16:53:59 +0000 (09:53 -0700)]
model: kill unneeded local variable

The "Thread *th" variable is used only on a few control paths, and it is never
reused. Might as well just calculate it on the fly. Also, it's recalculated and
masked by another local variable at a deeper level of nesting.

10 years agospacing
Brian Norris [Thu, 13 Sep 2012 16:42:54 +0000 (09:42 -0700)]
spacing

10 years agoMerge remote-tracking branch 'origin/makefile'
Brian Norris [Thu, 13 Sep 2012 16:21:08 +0000 (09:21 -0700)]
Merge remote-tracking branch 'origin/makefile'

10 years agolots of debugging here... finally working with my rmw example...
Brian Demsky [Thu, 13 Sep 2012 08:33:24 +0000 (01:33 -0700)]
lots of debugging here... finally working with my rmw example...

10 years agoMakefile: fixup Mac dependencies
Brian Norris [Thu, 13 Sep 2012 07:22:55 +0000 (00:22 -0700)]
Makefile: fixup Mac dependencies

Now, Mac OSX builds can just use "make", not "make mac". (This also allows
"make debug" for Mac OSX)

10 years agocleanup style
Brian Norris [Thu, 13 Sep 2012 07:01:01 +0000 (00:01 -0700)]
cleanup style

10 years agocommit new test case
Brian Demsky [Thu, 13 Sep 2012 05:59:03 +0000 (22:59 -0700)]
commit new test case

10 years agofix for horrible bug... turns out that we could generate an infinite set of bad...
Brian Demsky [Thu, 13 Sep 2012 05:57:00 +0000 (22:57 -0700)]
fix for horrible bug...  turns out that we could generate an infinite set of bad executions due to future values...
fix--don't send future values backwards until all of your promises are resolved...

10 years agomissing changes
Brian Demsky [Thu, 13 Sep 2012 05:08:22 +0000 (22:08 -0700)]
missing changes

10 years agoright fix for avoid rmw cycles... bad assumption in the cyclegraph
Brian Demsky [Thu, 13 Sep 2012 05:06:51 +0000 (22:06 -0700)]
right fix for avoid rmw cycles...  bad assumption in the cyclegraph

10 years agoanother bug fix...
Brian Demsky [Thu, 13 Sep 2012 04:03:37 +0000 (21:03 -0700)]
another bug fix...

10 years agoseparate out rmw actions
Brian Demsky [Thu, 13 Sep 2012 03:35:47 +0000 (20:35 -0700)]
separate out rmw actions
make sure we don't insert promises twice for a node

10 years ago(1) structure code a little better
Brian Demsky [Wed, 12 Sep 2012 23:24:07 +0000 (16:24 -0700)]
(1) structure code a little better
(2) add startChanges to cyclegraph...  This is just to check some assertions that rollback is being used correctly and doesn't rollback unintended changes

10 years agodeal with looping due to bogus future value via promise expiration
Brian Demsky [Wed, 12 Sep 2012 22:12:31 +0000 (15:12 -0700)]
deal with looping due to bogus future value via promise expiration
fix promise bug

10 years agofun issues...
Brian Demsky [Wed, 12 Sep 2012 09:52:34 +0000 (02:52 -0700)]
fun issues...
(1) need to compute promises for rmw nodes...they could satisfy them
(2) don't call rmwedge if you don't know where you are reading from yet
(3) miscopied commit from big merge (already_added -> !already_added)
(4) avoid adding rmw edges back to itself
(5) probably worth adding a check that the execution isfeasible before sending future values
(6) resolve promises should add rmwedges when appropriate
(7) fix seq_cst to mask earlier writes..

10 years agothreads, model, schedule: refactor thread joining
Brian Norris [Wed, 12 Sep 2012 02:48:38 +0000 (19:48 -0700)]
threads, model, schedule: refactor thread joining

The Thread can hold a list of ModelAction (instead of Threads) that are waiting
for its completion. This will give the exiting Thread a better ability to
handle the event.

This also deletes Scheduler::wait, since it is no superceded by Scheduler::sleep.

10 years agomodel: add ModelChecker::get_thread(ModelAction *act)
Brian Norris [Wed, 12 Sep 2012 02:45:57 +0000 (19:45 -0700)]
model: add ModelChecker::get_thread(ModelAction *act)

Many times, I need to convert ModelAction to a Thread. Overload get_thread() to
make it easier to use.

10 years agoschedule: add sleep() function
Brian Norris [Wed, 12 Sep 2012 02:38:50 +0000 (19:38 -0700)]
schedule: add sleep() function

The wait() and wake() functions are not very complementary. I will be removing
wait() in favor of a simpler sleep() function, which is introduced here.

10 years agocyclegraph: add non-NULL assertions
Brian Norris [Wed, 12 Sep 2012 00:54:29 +0000 (17:54 -0700)]
cyclegraph: add non-NULL assertions

10 years agoMerge branch 'demsky'
Brian Norris [Wed, 12 Sep 2012 00:52:02 +0000 (17:52 -0700)]
Merge branch 'demsky'

Branch cleaned up by Brian Norris

10 years agomodel: cleaning up some code
Brian Demsky [Tue, 11 Sep 2012 03:17:10 +0000 (20:17 -0700)]
model: cleaning up some code

10 years agomodel: handle RMW, unresolved reads in w_modification_order checks
Brian Norris [Tue, 11 Sep 2012 18:43:18 +0000 (11:43 -0700)]
model: handle RMW, unresolved reads in w_modification_order checks

10 years agomodel: fix the maxreads support
Brian Demsky [Mon, 10 Sep 2012 00:43:20 +0000 (17:43 -0700)]
model: fix the maxreads support

10 years agomodel: some bug fixes to the model checker
Brian Demsky [Sun, 9 Sep 2012 09:25:47 +0000 (02:25 -0700)]
model: some bug fixes to the model checker

10 years agolinuxrwlocks: two bug fixes; guess the model checker helps find bugs
Brian Demsky [Sun, 9 Sep 2012 09:25:47 +0000 (02:25 -0700)]
linuxrwlocks: two bug fixes; guess the model checker helps find bugs

10 years agomodel: bug fixes to new code
Brian Demsky [Sun, 9 Sep 2012 02:37:11 +0000 (19:37 -0700)]
model: bug fixes to new code

10 years agocyclegraph: support rolling back changes
Brian Demsky [Sun, 9 Sep 2012 02:37:11 +0000 (19:37 -0700)]
cyclegraph: support rolling back changes

10 years agomodel: replace action conditions with switch block
Brian Norris [Tue, 11 Sep 2012 19:24:15 +0000 (12:24 -0700)]
model: replace action conditions with switch block

10 years agomodel: add check_recency()
Brian Norris [Tue, 11 Sep 2012 17:20:06 +0000 (10:20 -0700)]
model: add check_recency()

Note the weaknesses of the code, as documented in @todo.

10 years agomodel: refactor "get next thread" code
Brian Norris [Tue, 11 Sep 2012 18:19:50 +0000 (11:19 -0700)]
model: refactor "get next thread" code

get_next_replay_thread() might as well handle all the Thread decisions for the
model-checker. Refactor, and rename to get_next_thread().

10 years agomodel: add too_many_reads flag
Brian Norris [Tue, 11 Sep 2012 17:19:46 +0000 (10:19 -0700)]
model: add too_many_reads flag

10 years agonodestack: add get_read_from_size()
Brian Norris [Tue, 11 Sep 2012 17:19:10 +0000 (10:19 -0700)]
nodestack: add get_read_from_size()

10 years agomain: add "maxreads" parameter
Brian Norris [Tue, 11 Sep 2012 17:10:39 +0000 (10:10 -0700)]
main: add "maxreads" parameter

10 years agomain: add parameter parsing
Brian Norris [Sat, 8 Sep 2012 07:38:03 +0000 (00:38 -0700)]
main: add parameter parsing

Only has a help message for now.

10 years agomodel: fix release sequence with RMW, acq vs. acq/rel
Brian Norris [Sat, 8 Sep 2012 06:36:00 +0000 (23:36 -0700)]
model: fix release sequence with RMW, acq vs. acq/rel

Check in a bugfix from Brian D

10 years agomodel: maintain a count of the pending lazy synchronizations
Brian Norris [Fri, 7 Sep 2012 20:12:46 +0000 (13:12 -0700)]
model: maintain a count of the pending lazy synchronizations

lazy_sync_size should be the sum of the size of all the lists in
lazy_sync_with_release.

10 years agomodel: group snapshottable ModelChecker members in struct
Brian Norris [Fri, 7 Sep 2012 19:58:06 +0000 (12:58 -0700)]
model: group snapshottable ModelChecker members in struct

These items shouldn't be reset individually, but rather should be grouped
together and allocated on the snapshotting heap. This puts us a step closer to
utilizing partial rollback within executions.

10 years agomodel: force THREAD_START to immediately follow THREAD_CREATE
Brian Norris [Fri, 7 Sep 2012 18:25:25 +0000 (11:25 -0700)]
model: force THREAD_START to immediately follow THREAD_CREATE

Note that on the current userprog.c test case, this change causes more
infeasible executions to appear. This is somewhat unexpected but probably just
a result of sub-optimal scheduling.

10 years agomodel: fix release_seq for open-ended synchronization
Brian Norris [Fri, 7 Sep 2012 17:38:58 +0000 (10:38 -0700)]
model: fix release_seq for open-ended synchronization

This fix handles the case where a thread may not yet have synchronized in a way
that ensures no future writes may break a release sequence. If we encounter
such a thread, we can return false (uncertain) and re-check this potential
release sequence later in the execution.

10 years agomodel: use std::find for release sequence search
Brian Norris [Fri, 7 Sep 2012 17:31:08 +0000 (10:31 -0700)]
model: use std::find for release sequence search

10 years agomodel: don't use global 'model' unnecessarily
Brian Norris [Fri, 7 Sep 2012 17:16:41 +0000 (10:16 -0700)]
model: don't use global 'model' unnecessarily

10 years agochanges
Brian Demsky [Fri, 7 Sep 2012 06:48:25 +0000 (23:48 -0700)]
changes

10 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Fri, 7 Sep 2012 01:56:39 +0000 (18:56 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

check in my stuff...

Conflicts:
model.cc
threads.h

10 years agochanges
Brian Demsky [Fri, 7 Sep 2012 01:32:56 +0000 (18:32 -0700)]
changes

10 years agoMerge branch 'norris'
Brian Norris [Thu, 6 Sep 2012 23:16:51 +0000 (16:16 -0700)]
Merge branch 'norris'

Fixes up some THREAD_JOIN behavior, cleaning up a little bit of general model-checker structure.

10 years agomodel: complete the Thread teardown during THREAD_FINISH
Brian Norris [Thu, 6 Sep 2012 21:07:44 +0000 (14:07 -0700)]
model: complete the Thread teardown during THREAD_FINISH

10 years agomodel: enforce rule: current_action != NULL
Brian Norris [Thu, 6 Sep 2012 21:04:09 +0000 (14:04 -0700)]
model: enforce rule: current_action != NULL

Now that I've fixed THREAD_JOIN, modify the comments and safety checks.

10 years agolibthreads: don't spin on THREAD_JOIN
Brian Norris [Thu, 6 Sep 2012 20:55:05 +0000 (13:55 -0700)]
libthreads: don't spin on THREAD_JOIN

THREAD_JOIN can now be implemented properly here. We shouldn't have to spin,
waiting for another thread to complete. This may help improve the ModelChecker
architecture, since we will never have NULL actions passed to the ModelChecker.

10 years agomodel: hook up THREAD_JOIN and THREAD_FINISH actions
Brian Norris [Thu, 6 Sep 2012 20:54:06 +0000 (13:54 -0700)]
model: hook up THREAD_JOIN and THREAD_FINISH actions

10 years agoschedule: add wait and wake functions
Brian Norris [Thu, 6 Sep 2012 20:37:35 +0000 (13:37 -0700)]
schedule: add wait and wake functions

These functions will be used to prevent execution of threads that should be
waiting for another event (e.g., a THREAD_JOIN should cause a thread to wait
for another thread's exit).

10 years agothreads: fixup THREAD_READY comment
Brian Norris [Thu, 6 Sep 2012 20:47:12 +0000 (13:47 -0700)]
threads: fixup THREAD_READY comment

This state will be used for more than just a context switch, so reword the
comment.

10 years agothreads: add THREAD_BLOCKED state
Brian Norris [Thu, 6 Sep 2012 20:41:12 +0000 (13:41 -0700)]
threads: add THREAD_BLOCKED state

To signal that a Thread cannot yet be added back to the Scheduler's ready list.

10 years agothreads: add a wait_list
Brian Norris [Thu, 6 Sep 2012 20:17:06 +0000 (13:17 -0700)]
threads: add a wait_list

This list will contain all Threads that are waiting on the current Thread. Will
be used for Thread joins, in particular.

10 years agothreads: add is_complete() helper function
Brian Norris [Thu, 6 Sep 2012 20:10:11 +0000 (13:10 -0700)]
threads: add is_complete() helper function

10 years agoaction: add THREAD_FINISH action
Brian Norris [Thu, 6 Sep 2012 20:07:26 +0000 (13:07 -0700)]
action: add THREAD_FINISH action

For cleanly finalizing a thread.

10 years agosnapshot-interface: debug prints: lengthen the "regionname" field
Brian Norris [Thu, 6 Sep 2012 18:43:06 +0000 (11:43 -0700)]
snapshot-interface: debug prints: lengthen the "regionname" field

10 years agoworking towards making datarace detection work
Brian Demsky [Thu, 6 Sep 2012 06:04:30 +0000 (23:04 -0700)]
working towards making datarace detection work

10 years agobug in race detector
Brian Demsky [Wed, 5 Sep 2012 07:27:23 +0000 (00:27 -0700)]
bug in race detector

10 years agoanother example
Brian Demsky [Wed, 5 Sep 2012 06:28:00 +0000 (23:28 -0700)]
another example

10 years agomodel: document ModelChecker::check_current_action
Brian Norris [Tue, 4 Sep 2012 21:13:28 +0000 (14:13 -0700)]
model: document ModelChecker::check_current_action

10 years agomodel: check_current_action returns its 'nextThread'
Brian Norris [Tue, 4 Sep 2012 20:08:46 +0000 (13:08 -0700)]
model: check_current_action returns its 'nextThread'

To begin some code structure rearrangements, I make check_current_action()
return the 'nextThread' value as a true return value. Eventually, the
nextThread field might not be needed, and the model-checker behavior might make
more sense...

10 years agomodel/schedule: revise 'nextThread' data flow
Brian Norris [Tue, 4 Sep 2012 19:45:49 +0000 (12:45 -0700)]
model/schedule: revise 'nextThread' data flow

The ModelChecker::nextThread field was being abused a little in my aging
design. It really should be either a private field (not accessed even via
accessors) or else just a return value / function parameter.

This commit makes a change so that nextThread is a Thread pointer and is
directly supplied to the Scheduler. If it is NULL, then the Scheduler is
allowed to pick its own Thread to run.

10 years agoaction: print '?' for unknown read-from-future
Brian Norris [Tue, 4 Sep 2012 17:59:47 +0000 (10:59 -0700)]
action: print '?' for unknown read-from-future

To provide more informative debugging traces, use a placeholder '?' as the "Rf"
value when printing a 'read' ModelAction that has no reads-from value. This
helps, for instance, when manually identifying problem points in an infeasible
execution.

10 years agomodel: re-check release sequences lazily
Brian Norris [Fri, 24 Aug 2012 00:54:39 +0000 (17:54 -0700)]
model: re-check release sequences lazily

For now, I write this "lazy check" as follows:

Whenever one of the following occurs:
* a Promise is fulfilled
* a mo_graph edge is added

Then I recheck all the actions (for the relevant object location) that are
waiting in the lazy release head queue.

10 years agomodel: add resolve_release_sequences() function
Brian Norris [Sat, 25 Aug 2012 01:37:15 +0000 (18:37 -0700)]
model: add resolve_release_sequences() function

This function can check for release sequence resolutions then propagate
synchronization and remove from the "lazy release" list. It does not add any
new mo_graph edges yet.

10 years agomodel: stash actions for lazy release-seq checking
Brian Norris [Thu, 23 Aug 2012 02:16:58 +0000 (19:16 -0700)]
model: stash actions for lazy release-seq checking

Build up lists of actions to lazily check for new release sequence
developments.

10 years agomodel: report 'updates' when adding mo_graph edges
Brian Norris [Fri, 24 Aug 2012 00:47:31 +0000 (17:47 -0700)]
model: report 'updates' when adding mo_graph edges

The rest of the model checker would like to know if any edges were added. Add a
boolean return value to report this.

10 years agomodel: report status of resolved promises
Brian Norris [Fri, 24 Aug 2012 00:50:21 +0000 (17:50 -0700)]
model: report status of resolved promises

The rest of the model checker needs to know when promises are added, so add a
return status as a boolean.

10 years agoaction, clockvector: add 'has_synchronized_with()' functions
Brian Norris [Thu, 23 Aug 2012 19:31:08 +0000 (12:31 -0700)]
action, clockvector: add 'has_synchronized_with()' functions

These functions will check whether a ClockVector (or corresponding ModelAction)
is *completely* synchronized with another already. This is different from
simply "happens before," because I may need to update and propagate a clock
vector after initial execution as more information becomes available, and so
this function helps determine whether a particular pair of vectors is worth
merging (and then - expensively - propagating) before actually performing the
synchronization.

[Not documented properly yet...]

10 years agoaction: make synchronize_with() public
Brian Norris [Thu, 23 Aug 2012 19:30:27 +0000 (12:30 -0700)]
action: make synchronize_with() public