On Monday 14 April 2008 06:55, Attila Szegedi wrote:
> On 2008.04.14., at 15:42, Randall R Schulz wrote:
> > As far as it being single-threaded, when running as a CLI command,
> > it is
> > (JVM threads notwithstanding), and in that setting it's no big deal
> > if OOM handling is disorderly. The user can simply re-run the
> > program with
> > different limits (memory or operation count). But when it runs in a
> > servlet container, there are potentially other threads executing
> > competing user request as well as whatever other threads the
> > servlet container uses to do its things.
> But then the concurrent users interfere with each others'
> computations, don't they? If a user is lucky enough to hit the server
> with a request when nobody else does, he'll get to utilize more
> memory (and potentially arrive at a different answer) than if he hits
> the server when 10 other people do, and have all of their
> computations compete for memory. That does sound like an unfortunate
> trait in a webapp.
Yes, that's true, but it's an inherent problem. I could devise a scheme
wherein I configure support for up to N concurrent requests and let
each request get only 1/N of the available heap, but that would be
excessively conservative most of the time.
And now that I've solved my "unpredictability" problems (see last week's
threads if you're interested), for a given problem one either gets the
answer or no answer, not different answers.
Ultimately, it's intended that each user will have their own instance of
the prover and its supporting content repository and browser-based
interface. But in the interim, there's a shared host with all the
attendendant problems of resource competition.
I think part of the problem here is that people are seeing this as a
typical e-commerce web-app, but that's really not the cases. It's not
primarily a content-oriented application (characterized mostly by
database access and presentation), but rather an interface to a compute
engine (a theorem prover). This is a research project for which the
web-app is not the central emphasis, but rather a necessary adjunct. I
cannot afford to put a great deal of effort into making it
production-quality. I have to make do with "good enough." I don't like
it, but we're on a shoestring.